Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR07-055 | 16th November 2008 00:00

Constraint satisfaction problems in clausal form: Autarkies, deficiency and minimal unsatisfiability

RSS-Feed




Revision #1
Authors: Oliver Kullmann
Accepted on: 16th November 2008 00:00
Downloads: 1648
Keywords: 


Abstract:

Many editorial improvements and literature updates.


Paper:

TR07-055 | 22nd May 2007 00:00

Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability


Abstract:

We consider the next step from boolean conjunctive normal forms to
arbitrary constraint satisfaction problems (with arbitrary constraints), namely "generalised clause-sets" (or "sets of no-goods"), which allow negative literals "v <> e" for variables v and values e --- this level of generality appears to be the right level for studying *combinatorial properties*. 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 is provided.

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. We obtain fixed parameter tractability (FPT) of satisfiability decision for generalised clause-sets, using as parameter the maximal deficiency (over all sub-clause-sets).

Another central result regarding the deficiency in the boolean case is the classification of minimally unsatisfiable clause-sets with low deficiency (MU(1), MU(2), ... for the class of minimally unsatisfiable clause-sets of deficiency 1, 2, ...). We generalise the well-known characterisations of boolean MU(1).

The proofs for FPT and MU(1) actually are not straight-forward, but are obtained by an interplay between suitable generalisations of techniques and notions from the boolean case, and exploiting combinatorial properties of the natural translation of (generalised) clause-sets into boolean clause-sets.

Of fundamental importance here is *autarky theory*, and we concentrate especially on matching autarkies (based on matching theory). A natural problem is to determine the structure of (matching) lean clause-sets (which do not admit non-trivial (matching) autarkies), and we give
several characterisations.

Minimally unsatisfiable (generalised) clause-sets are lean, and we also consider the generalisation to irredundant clause-sets, taking into account satisfiable clause-sets. Of special interest are hitting clause-sets (which are irredundant in a very strong sense) and the generalisation to multihitting clause-sets (generalising the hypergraph transversal problem). Again, several characterisations and properties are established.

We close with a discussion of open problems.



ISSN 1433-8092 | Imprint