Journal article 1223 views
Constraint satisfaction problems in clausal form I: Autarkies and deficiency.
Oliver Kullmann 
Fundamenta Informaticae, Volume: 109, Issue: 1, Pages: 27 - 81
Swansea University Author:
Oliver Kullmann
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.3233/FI-2011-428
Abstract
We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown “signed literals...
| Published in: | Fundamenta Informaticae |
|---|---|
| ISSN: | 0169-2968 |
| Published: |
2011
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa5283 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown “signed literals”, corresponding to unary constraints in CSP. However we argue that only the restricted form of “negative monosigned literals” and the resulting generalised clause-sets, corresponding to “sets of no-goods” in the AI literature, maintain the essential properties of boolean conjunctive normal forms. In this first part of a mini-series of two articles, we build up a solid foundation for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. Autarky theory plays a fundamental role here, and we concentrate especially on matching autarkies (based on matching theory). A natural task is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. A central result is the computation of the lean kernel (the largest lean subset) of a (generalised) clause-set in polynomial time for bounded maximal deficiency. |
|---|---|
| College: |
Faculty of Science and Engineering |
| Issue: |
1 |
| Start Page: |
27 |
| End Page: |
81 |