The SAT problem is the first problem proven to be -Complete. However, many instances of this problem with certain properties can be solved efficiently in polynomial time. Well-known examples of such easy instances are 2-sat and horn formulas. All clauses in a 2-sat formula have at most 2 literals and horn-formulas consist only of clauses that contain at most one positive literal. In other words, a 2-sat clause is a conjunction of two implications and any horn clause can be rewritten as a conjunction of positive literals that implies either false or a negative literal. It may seem that satisfiability of formulas containing both 2-sat as well as horn clauses can be decided in polynomial time, however, because of the -completeness that we will prove shortly, this is not the case unless . The problem also remains -complete for Dual-horn clauses instead of normal horn clauses.
The problem mentioned above can be formally formulated as follows:
Input: A formula in conjunctive normal form (CNF), that consists only of 2-sat or horn clauses.
Question: Is satisfiable?
Example of a formula that contains only 2-sat or horn clauses:
The first 6 clauses are 2-sat clauses and the last one is a horn clause, this formula is satisfiable.
Proof of NP-Completeness
This problem is a special case of the
SAT problem and is therefore also in (the variable assignment can be used as a certificate and it can be verified in polynomial time).
We will now construct a reduction from the
3-SAT problem. Consider an arbitrary 3-sat clause. If it contains at most 2 literals, that it is directly a 2-sat clause. If there is at most one positive literal, then it is already a horn clause. Therefore, we need to find equisatisfiable sets of clauses for the following situations:
- Two positive literals:
- Three positive literals:
By using the idea of the Tseitin transformation for the first case, it follows that is satisfiable iff is satisfiable, this can be rewritten as:
As regards the second case, we can use the result from the first case to produce a horn-clause:
This is clearly a polynomial-time reduction.
Dual Horn-sat and 2-sat clauses
The above problem remains -complete if we consider Dual-horn clauses instead of (normal) Horn clauses (a clause is called Dual-horn, if it has at most one negative literal).
Analogously to the proof above, in order to prove -hardness we have to express 3-sat clauses with 2 and 3 negative literals in terms of 2-sat and dual-horn clauses. If the clause has 2 negative literals, then:
Normally, in the Tseitin transformation we make the introduced variables equisatisfiable with the corresponding sub-formula. Here, in order to prevent in the horn clause, we make equisatisfiable with .
If the clause has 3 negative literals, then we use the same trick two times: