Axioms of Minimum Size Resolution Refutations

Question

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.

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