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

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

CC BY-SA 4.0
2019-05-21T18:47:27.363Z
2019-05-21T18:47:27.363Z
Jakob Nordstrom
<p>Let <span class="math-container">$\phi$</span> be an unsatisfiable CNF formula and let <span class="math-container">$\Pi$</span> be a resolution refutation of <span class="math-container">$\phi$</span> of minimum size. Let <span class="math-container">$\psi$</span> be the subformula of <span class="math-container">$\phi$</span> containing the clauses that actually appear as axioms in <span class="math-container">$\Pi$</span>. Is there anything interesting that can be said about <span class="math-container">$\psi$</span>?</p>

<p>Some specific questions:</p>

<ul>
<li>Is <span class="math-container">$\psi$</span> minimally unsatisfable? (i.e., are all proper subsets of <span class="math-container">$\psi$</span> satisfiable?)</li>
<li>Are all variables appearing in <span class="math-container">$\psi$</span> necessary for unsatisfiability? (i.e., is there an assignment to all but one variable that does not falsify any clauses in <span class="math-container">$\psi$</span>?)</li>
<li>Is <span class="math-container">$\psi$</span> a minimum unsatisfiable core of <span class="math-container">$\phi$</span>?</li>
</ul>

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

CC BY-SA 4.0
2019-05-17T13:25:17.690Z
What is an unsatiafiable core?
Joshua Grochow
CC BY-SA 4.0
2019-05-17T20:35:17.967Z
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.
Nathan
<sat><proof-complexity><resolution>
Axioms of Minimum Size Resolution Refutations
Nathan
# Axioms of Minimum Size Resolution Refutations

(Asked by: username_0 on 2019-05-16)

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.

**Tags:** sat, proof-complexity, resolution

> **Comments:**
> **username_1**: What is an unsatiafiable core?  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_2 on 2019-05-21. Score: 6 | Accepted answer

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


---

