<p><em>Resolution</em> in this context is broader than unit propagation, since a 2-CNF might not have any unit clauses. Instead resolution refers to the inference rule that given a pair of clauses $C = (x \vee y), \hat{C} = (\neg x \vee z)$ that contain a variable and its negation respectively, we can infer the new clause $(y \vee z)$. In addition, let $(x \vee x), (\neg x \vee \neg x)$ infer the empty clause $()$ which we will declare not satisfiable.</p>

<p>See <a href="https://cstheory.stackexchange.com/a/6891/8985">here</a> for an excellent explanation of why repeated application of this resolution rule will always lead to the empty clause iff the 2-CNF was unsatisfiable. </p>

<p>If the 2-CNF is satisfiable, then set $z_C = 1$ for every clause $C$ occurs in or that is inferred by resolution on the 2-CNF, and $0$ for every other clause. Every implication is satisfied, and every unit clause is satisfied. So the Horn formula is satisfied.</p>

<p>If the 2-CNF formula is unsatisfiable, then resolution will generate the empty clause. By the implications in the generated Horn formula, setting $z_C=1$ for each clause $C$ in the 2-CNF implies $z_{empty}=1$. But the unit clause $\neg z_{empty}$ prohibits this. Therefore, the Horn formula is unsatisfiable.</p>

CC BY-SA 3.0
2015-12-03T10:54:53.483Z
2015-12-03T10:54:53.483Z
2017-04-13T12:32:28.743Z
Joe Bebel
<p>In the question, <a href="https://cstheory.stackexchange.com/questions/200">Translating SAT to HornSAT</a>, Martin Seymour gives <a href="https://cstheory.stackexchange.com/questions/200/27517#27517">a method due to Joshua Grochow</a>.  It transforms 2-SAT into Horn-SAT, by creating a variable for every possible 2-SAT clause.  Then, if a clause (or new variable) follows from two other clauses (variables) from "a single resolution step", it adds this implication to the formula.  Finally, the unit clauses are added, along with a clause signifying not empty.</p>

<p>Can someone please explain, in detail, why we add clauses from "single resolution steps"?  Am I correct in assuming that this means a single resolution step from unit propagation?  Also, and perhaps most importantly, can someone prove that this method works?</p>

<p>Essentially, I'd like to know everything I can to ensure that I can implement this method, and also prove that it works.  I'm also wondering if perhaps this method can be found in the literature somewhere.</p>

<reference-request><sat>
Can we confirm that 2-SAT can indeed be transformed into Horn-SAT in this manner?
Matt Groff
# Can we confirm that 2-SAT can indeed be transformed into Horn-SAT in this manner?

(Asked by: username_0 on 2015-12-02)

In the question, [Translating SAT to HornSAT](https://cstheory.stackexchange.com/questions/200), Martin Seymour gives [a method due to Joshua Grochow](https://cstheory.stackexchange.com/questions/200/27517#27517). It transforms 2-SAT into Horn-SAT, by creating a variable for every possible 2-SAT clause. Then, if a clause (or new variable) follows from two other clauses (variables) from "a single resolution step", it adds this implication to the formula. Finally, the unit clauses are added, along with a clause signifying not empty.

Can someone please explain, in detail, why we add clauses from "single resolution steps"? Am I correct in assuming that this means a single resolution step from unit propagation? Also, and perhaps most importantly, can someone prove that this method works?

Essentially, I'd like to know everything I can to ensure that I can implement this method, and also prove that it works. I'm also wondering if perhaps this method can be found in the literature somewhere.

**Tags:** reference-request, sat

---

## 1 answers

### Answer by username_1 on 2015-12-03. Score: 7

*Resolution* in this context is broader than unit propagation, since a 2-CNF might not have any unit clauses. Instead resolution refers to the inference rule that given a pair of clauses $C = (x \vee y), \hat{C} = (\neg x \vee z)$ that contain a variable and its negation respectively, we can infer the new clause $(y \vee z)$. In addition, let $(x \vee x), (\neg x \vee \neg x)$ infer the empty clause $()$ which we will declare not satisfiable.

See [here](https://cstheory.stackexchange.com/a/6891/8985) for an excellent explanation of why repeated application of this resolution rule will always lead to the empty clause iff the 2-CNF was unsatisfiable.

If the 2-CNF is satisfiable, then set $z\_C = 1$ for every clause $C$ occurs in or that is inferred by resolution on the 2-CNF, and $0$ for every other clause. Every implication is satisfied, and every unit clause is satisfied. So the Horn formula is satisfied.

If the 2-CNF formula is unsatisfiable, then resolution will generate the empty clause. By the implications in the generated Horn formula, setting $z\_C=1$ for each clause $C$ in the 2-CNF implies $z\_{empty}=1$. But the unit clause $\neg z\_{empty}$ prohibits this. Therefore, the Horn formula is unsatisfiable.


---

