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.


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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.