Let $\phi$ be an unsatisfiable CNF formula and let $\Pi$ be a resolution refutation of $\phi$ of minimum size. Let $\psi$ be the subformula of $\phi$ containing the clauses that actually appear as axioms in $\Pi$. Is there anything interesting that can be said about $\psi$?

Some specific questions:

  • Is $\psi$ minimally unsatisfable? (i.e., are all proper subsets of $\psi$ satisfiable?)
  • Are all variables appearing in $\psi$ necessary for unsatisfiability? (i.e., is there an assignment to all but one variable that does not falsify any clauses in $\psi$?)
  • Is $\psi$ a minimum unsatisfiable core of $\phi$?

All of these properties seem unlikely to hold in general but I cannot think of any counterexamples.

  • $\begingroup$ What is an unsatiafiable core? $\endgroup$ May 17, 2019 at 13:25
  • 1
    $\begingroup$ An unsatisfiable core is just a subformula that is unsatisfiable. So for the third question, I am just interested if the $\psi$ can always be assumed to be minimum in size. $\endgroup$
    – Nathan
    May 17, 2019 at 20:35

1 Answer 1


With the caveat that I am posting this quickly in a sleep-deprived state, I think the answer is "no" to all three questions.

Take the pigeonhole principle formulas PHP^m_n for m pigeons and n holes. The miniminal length of a resolution refutation for m = n+1 is exp(Omega(n)) by Haken. However, Buss and Pitassi proved that for m = exp(\sqrt(n log n)) pigeons (or something in that range) there are refutations of length exp(\sqrt(n log n)) (or something in that range). Clearly, then, the shortest resolution refutation in this case is using lots of redundant clauses (from the point of view of minimal unsatisfiability).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.