__
TR07-055 | 22nd May 2007 00:00
__

#### Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability

TR07-055
Authors:

Oliver Kullmann
Publication: 22nd June 2007 11:35

Downloads: 1470

Keywords:

(multi)hitting clause-sets,

autarky theory,

boolean translation,

clausal form,

constraint satisfaction,

deficiency,

fixed parameter tractability,

irredundant clause-sets,

matching autarky,

SAT problem,

signed formulas
**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.