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

Stefan Szeider

The deficiency of a propositional formula F in CNF with n variables

and m clauses is defined as m-n. It is known that minimal

unsatisfiable formulas (unsatisfiable formulas which become

satisfiable by removing any clause) have positive deficiency.

Recognition of minimal unsatisfiable formulas is NP-hard, and it was

shown recently ...
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 >>>