3. 3SAT vs 2SAT

NSAT Problem

We may restrict the number of literals in each clause to be able to use more efficient algorithms to solve SAT, e.g. for some Boolean Satisfiability Problem NSAT:

• Input: propositional formula $F$ in CNF with at most $N$ literals in each clause
• Output: $\top$ if and only if $F$ is satisfiable

NSAT Theorems

Theorem: This also produces a chain of polynomial reductions:

$$2SAT{\le }_{p}3SAT{\le }_{p}4SAT{\le }_p\dots {\le }_{p}kSAT{\le }_p\dots {\le }_{p}SAT$$

Proof: This reduction is easy since every CNF formula with at most $k$ literals in each clause also has at most $(k+1)$ literals in each clause.

Theorem: We also have a chain of polynomial reactions going the other way:

$$SAT{\le }_p\dots {\le }_{p}kSAT{\le }_p\dots {\le }_{p}5SAT{\le }_{p}4SAT{\le }_{p}3SAT$$

Proof: It is enough to show that $SAT{\le }_{p}3SAT$ because $(k+1)SAT{\le }_{p}SAT{\le }_{p}3SAT{\le }_{p}kSAT$

1. Let $F$ be an arbitrary formula in CNF: $(P\vee \neg Q\vee R\vee S)\wedge (Q\vee \neg R\vee \neg T)$
2. Find a clause which contains more than 3 literals: $(P\vee \neg Q\vee R\vee S)$
3. Introduce a new propositional variable to break up this clause: $$(P\vee \neg Q\vee X)\wedge (\neg X\vee R\vee S)$$
4. Repeat until all clauses contain at most 3 literals.

Solving 2SAT

Theorem: 2SAT is solvable in polynomial time Proof: we can solve 2SAT by using the Strongly Connected Component algorithm

1. Write each clause as two implications: $$(A\vee B)\equiv (\neg A\to B)\wedge (\neg B\to A)$$
2. Construct the implication graph: (the edges represent implications)
3. If any vertex / literal is true, then all nodes that it directs to must also be true as per the implication. It follows strongly connected components must either be assigned true or false under any assignment.
4. Check whether any SCC contains a literal and its negation:
5. Since we can compute and check each strongly connected component in polynomial time, we have that 2SAT is solvable in polynomial time.

Easy variants of SAT

• (Definite) Propositional Horn clause Every clause contains exactly one positive literal Every clause can be written in implication form with a single positive head