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.