<p>Yes, any unsatisfiable Horn CNF has a tree-like resolution refutation with a linear number of clauses.</p>
<p>Consider the standard poly-time Horn-SAT algorithm, which works as follows. First, set all variables to false. Repeat: pick an unsatisfied clause; if it's negative, answer UNSATISFIABLE; otherwise, set its positive literal to true. If all clauses are satisfied, answer SATISFIABLE.</p>
<p>Assume the input formula is unsatisfiable. If you look at the order in which the algorithm sets variables to true, as well as the offending clauses that make it so, you obtain a list of pairwise distinct variables
<span class="math-container">$$x_0,\dots,x_{t-1}$$</span>
and input clauses
<span class="math-container">$$C_0,\dots,C_t$$</span>
such that
<span class="math-container">$$C_i\subseteq\{\neg x_j:j&lt;i\}\cup\{x_i\},\qquad i&lt;t,$$</span>
and
<span class="math-container">$$C_t\subseteq\{\neg x_j:j&lt;t\}.$$</span>
Construct a tree-like resolution refutation as follows: resolve <span class="math-container">$D_t:=C_t$</span> and <span class="math-container">$C_{t-1}$</span> over the <span class="math-container">$x_{t-1}$</span> variable, obtaining <span class="math-container">$D_{t-1}$</span>; resolve <span class="math-container">$D_{t-1}$</span> and <span class="math-container">$C_{t-2}$</span> over <span class="math-container">$x_{t-2}$</span> to get <span class="math-container">$D_{t-2}$</span>; etc., in the last step resolving <span class="math-container">$D_1$</span> and <span class="math-container">$C_0$</span> over <span class="math-container">$x_0$</span> to get <span class="math-container">$D_0$</span>. By reverse induction on <span class="math-container">$i\le t$</span>, we see that
<span class="math-container">$$D_i\subseteq\{\neg x_j:j&lt;i\}.$$</span>
In particular, <span class="math-container">$D_0$</span> is the empty clause.</p>
<p>Thus, you obtain a refutation of the input formula <span class="math-container">$\phi$</span> whose number of clauses is at most twice the number of distinct variables positively occuring in <span class="math-container">$\phi$</span>, and whose total size is thus at most quadratic in the size of <span class="math-container">$\phi$</span>.</p>

CC BY-SA 4.0
2024-03-06T13:43:06.580Z
(1) Obviously I have no idea what you may have studied. This is the standard HornSAT algorithm that you can find described in many places, see e.g. https://tryalgo.org/en/satisfiability/2016/12/04/horn-sat/ or https://en.wikipedia.org/wiki/Horn-satisfiability (the latter presents it differently so that the clauses are restricted in the process instead of just maintaining the assignment, but the underlying algorithm is the same). (2) It may easily happen that $D_{i+1}$ does not actually contain $\neg x_i$. This does not matter. If one or both of the principal literals of an instance of the ...
Emil Jeřábek
CC BY-SA 4.0
2024-03-06T13:45:40.720Z
... resolution rule are missing, this resolution inference degenerates to an instance of weakening, which can be skipped.
Emil Jeřábek
CC BY-SA 4.0
2024-02-14T19:35:47.020Z
2024-02-14T22:50:24.357Z
2024-02-14T22:50:24.357Z
Emil Jeřábek
<p>Recall that a CNF formula is Horn if each clause contains at most one positive literal.</p>
<p>Is it possible any unsatisfiable Horn CNF formula has a polynomial-size treelike Resolution refutation? Is there any proof exists in any paper?</p>

<reference-request><proof-complexity><resolution>
Horn clause on cnf
David
# Horn clause on cnf

(Asked by: username_0 on 2024-02-14)

Recall that a CNF formula is Horn if each clause contains at most one positive literal.

Is it possible any unsatisfiable Horn CNF formula has a polynomial-size treelike Resolution refutation? Is there any proof exists in any paper?

**Tags:** reference-request, proof-complexity, resolution


---

## 1 answers

### Answer by username_1 on 2024-02-14. Score: 5 | Accepted answer

Yes, any unsatisfiable Horn CNF has a tree-like resolution refutation with a linear number of clauses.

Consider the standard poly-time Horn-SAT algorithm, which works as follows. First, set all variables to false. Repeat: pick an unsatisfied clause; if it's negative, answer UNSATISFIABLE; otherwise, set its positive literal to true. If all clauses are satisfied, answer SATISFIABLE.

Assume the input formula is unsatisfiable. If you look at the order in which the algorithm sets variables to true, as well as the offending clauses that make it so, you obtain a list of pairwise distinct variables
$$x\_0,\dots,x\_{t-1}$$
and input clauses
$$C\_0,\dots,C\_t$$
such that
$$C\_i\subseteq\{\neg x\_j:j
and
$$C\_t\subseteq\{\neg x\_j:j
Construct a tree-like resolution refutation as follows: resolve $D\_t:=C\_t$ and $C\_{t-1}$ over the $x\_{t-1}$ variable, obtaining $D\_{t-1}$; resolve $D\_{t-1}$ and $C\_{t-2}$ over $x\_{t-2}$ to get $D\_{t-2}$; etc., in the last step resolving $D\_1$ and $C\_0$ over $x\_0$ to get $D\_0$. By reverse induction on $i\le t$, we see that
$$D\_i\subseteq\{\neg x\_j:j
In particular, $D\_0$ is the empty clause.

Thus, you obtain a refutation of the input formula $\phi$ whose number of clauses is at most twice the number of distinct variables positively occuring in $\phi$, and whose total size is thus at most quadratic in the size of $\phi$.

> **Comments:**
> **username_1**: (1) Obviously I have no idea what you may have studied. This is the standard HornSAT algorithm that you can find described in many places, see e.g. https://tryalgo.org/en/satisfiability/2016/12/04/horn-sat/ or https://en.wikipedia.org/wiki/Horn-satisfiability (the latter presents it differently so that the clauses are restricted in the process instead of just maintaining the assignment, but the underlying algorithm is the same). (2) It may easily happen that $D_{i+1}$ does not actually contain $\neg x_i$. This does not matter. If one or both of the principal literals of an instance of the ...  
> **username_1**: ... resolution rule are missing, this resolution inference degenerates to an instance of weakening, which can be skipped.  

---

