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

Jakob NordstrÃ¶m, Alexander Razborov

In the context of proving lower bounds on proof space in $k$-DNF

resolution, [Ben-Sasson and Nordström 2009] introduced the concept of

minimally unsatisfiable sets of $k$-DNF formulas and proved that a

minimally unsatisfiable $k$-DNF set with $m$ formulas can have at most

$O((mk)^{k+1})$ variables. They also gave an example of ...
more >>>