Can we confirm that 2-SAT can indeed be transformed into Horn-SAT in this manner?

Question

In the question, Translating SAT to HornSAT, Martin Seymour gives a method due to Joshua Grochow. 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.

Answer 1

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