Many editorial improvements and literature updates.
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.