2-SAT4 Algorithm by Literal Enumeration

Definition

2-SAT4 Algorithm by Literal Enumeration

Given a 2-SAT4 instance, write
$F=F_{\le 2}\wedge C_1\wedge \cdots \wedge C_k,k\le 4,$
where $F_{\le 2}$ contains all clauses of size at most two and $C_1,\dots ,C_k$ are the longer clauses. Enumerate one literal ${\ell }_j\in C_j$ per long clause and test the 2-SAT formula
$F_{{\ell }_1,\dots ,{\ell }_k}=F_{\le 2}\wedge {\ell }_1\wedge \cdots \wedge {\ell }_k.$
Accept if at least one test is satisfiable. Because $k\le 4$ is fixed, the algorithm runs in polynomial time.

Construction of the tests

Separate the long clauses without forgetting them

Clauses of length zero, one or two stay in $F_{\le 2}$. An empty clause makes the input unsatisfiable immediately. Deleting the long clauses alone is not enough: an assignment satisfying the remaining formula may violate them.

Instead, choose a witness literal for each long clause. For example, let
$F_{\le 2}=(\neg a\vee \neg d),C_1=(a\vee b\vee c),C_2=(d\vee e\vee f).$

The tuple $(a,d)$ asks whether the short clauses can be satisfied while both $a$ and $d$ are true. It does not assign all other variables. Choosing one witness per clause also does not require every other literal in that clause to be false.

Force each chosen witness using a unit clause

For tuple $({\ell }_1,\dots ,{\ell }_k)$, add the unit clauses $({\ell }_1),\dots ,({\ell }_k)$ to $F_{\le 2}$. The resulting formula still has at most two literals per clause, so a 2-SAT solver applies.

Different clauses may produce repeated or contradictory witness literals. Repeated unit clauses are harmless; contradictory units make that test unsatisfiable. Neither case requires a special correctness argument outside the solver.

Pseudocode

split F into short clauses F_short and long clauses C[1],...,C[k]
if F contains an empty clause:
    return NO
 
for each tuple (l[1],...,l[k]) in C[1] × ... × C[k]:
    H = F_short AND (l[1]) AND ... AND (l[k])
    if TwoSAT(H) returns YES:
        return YES
 
return NO

When $k=0$, the product contains exactly one empty tuple. The algorithm therefore runs the solver once on $F_{\le 2}=F$, rather than performing zero tests.

Correctness

A successful test exists exactly when the original formula is satisfiable

Forward: choose witnesses from a satisfying assignment

Let $\alpha \models F$. Each long clause $C_j$ has some true literal ${\ell }_j$. The algorithm enumerates that tuple. The same assignment satisfies $F_{\le 2}$ and every unit clause ${\ell }_j$, so its test returns yes.

Backward: a successful test satisfies the deleted clauses too

Suppose a test has satisfying assignment $\alpha$. It satisfies all short clauses. For each long clause $C_j$, the test forces ${\ell }_j$ true, and ${\ell }_j\in C_j$. Thus $C_j$ is satisfied. Consequently $\alpha \models F$.

Running time

Let $L$ be the total number of literal occurrences in the input, and put $S=1+n+m+L$, where $n$ is the number of variables and $m$ the number of clauses. This structural size is polynomially bounded by the input encoding length.

For $k\ge 1$, the number of tests is

$$\underset{\text{one choice per long clause}}{\underbrace{\prod _{j=1}^k|C_j|}}\le S^k\le S^4.$$

For $k=0$ it is $1$. Each test has size $O(S)$ and is solvable in $O(S)$ graph operations by the implication-graph algorithm for 2-SAT. Thus the total bound is $O(S^5)$ operations, including constructing the tests. Encoding and indexing overhead remains polynomial.

The fixed bound on the number of long clauses is essential to this analysis. If $k$ were part of the input, the bound $O(S^{k+1})$ would not be a polynomial with a fixed exponent.

Reduction type

The construction produces a polynomial-sized family of 2-SAT instances and accepts if any one is satisfiable. It is therefore a polynomial-time disjunctive Turing reduction: the solver answers are combined by logical OR. All queries can be prepared in advance, so they are nonadaptive.

This construction is not itself a Karp reduction, which must output one target instance with the same yes/no answer. This distinction concerns the construction, not an impossibility of a Karp reduction: once a polynomial decision algorithm is available, one can decide the source and output a fixed satisfiable or unsatisfiable 2-SAT formula.