Oliver Kullmann

A basic property of minimally unsatisfiable clause-sets F is that

c(F) >= n(F) + 1 holds, where c(F) is the number of clauses, and

n(F) the number of variables. Let MUSAT(k) be the class of minimally

unsatisfiable clause-sets F with c(F) <= n(F) + k.

Poly-time decision algorithms are known ... more >>>

Oliver Kullmann

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 ...
more >>>