SAT and 3-SAT

A Boolean formula is built from variables $x_1, x_2, \dots, x_n$, each taking value TRUE (1) or FALSE (0), combined with the connectives AND ($\land$), OR ($\lor$), and NOT ($\lnot$). A literal is a variable or its negation, e.g. $x_3$ or $\lnot x_3$. The satisfiability problem (SAT) asks: given a formula $\varphi$, does there exist an assignment of truth values to its variables under which $\varphi$ evaluates to TRUE? If such an assignment exists, $\varphi$ is satisfiable; otherwise it is unsatisfiable. Most treatments of SAT restrict attention to conjunctive normal form (CNF): a formula that is an AND of clauses, where each clause is an OR of literals. For example,

is in CNF with three clauses. CNF is a universal normal form — any Boolean formula can be converted to an equivalent-satisfiability CNF formula in polynomial time (via the Tseitin transformation, introducing auxiliary variables), so restricting SAT to CNF inputs loses no generality for complexity purposes. 3-CNF further restricts every clause to have exactly three literals (over possibly repeated or negated variables); 3-SAT is the satisfiability problem restricted to 3-CNF formulas. Formally, as decision problems:

Both languages live in NP: a satisfying assignment serves as a polynomially-sized certificate, and checking that an assignment satisfies a formula is a simple linear scan. The deep result — the Cook-Levin Theorem — is that SAT is not merely in NP but NP-complete: every language decidable by a nondeterministic polynomial-time Turing machine reduces to SAT in polynomial time. This makes SAT a "universal" problem for NP: solving SAT in polynomial time would imply P = NP. A further reduction shows 3-SAT is NP-complete too, which is why 3-SAT — not general SAT — is the typical starting point when proving new problems NP-complete (as later used for Classic NP-Complete Problems: Clique and Vertex Cover).

There are two algorithmic stories to tell for SAT: the polynomial-time verifier, which places SAT in NP, and the exponential-time search/decision procedures actually used to solve it (since no polynomial algorithm is known). Both are worth understanding precisely.

Verification. Given a formula $\varphi$ in CNF with $m$ clauses over $n$ variables, and a candidate assignment $a: \{x_1,\dots,x_n\} \to \{0,1\}$, checking $a \models \varphi$ requires evaluating each clause (a clause is TRUE if at least one of its literals is TRUE under $a$) and taking the AND over all clauses. ``` Verify-SAT(φ, a):

# φ is a CNF formula: list of clauses; each clause is a list of literals

# a is an assignment: array indexed by variable, value in {0,1} for each clause C in φ: clauseSatisfied ← false for each literal ℓ in C: if ℓ = x_i and a[i] = 1: clauseSatisfied ← true break if ℓ = ¬x_i and a[i] = 0: clauseSatisfied ← true break if not clauseSatisfied: return false # this clause is false ⇒ φ is false return true # every clause satisfied ⇒ φ is satisfied ``` This runs in time proportional to the total number of literal occurrences, which is $O(m \cdot k)$ for clause length $k$ (constant $k=3$ for 3-SAT), hence polynomial — this is exactly what places SAT and 3-SAT in NP.

Search (brute force, and the standard reduction argument for 3-SAT from SAT). No known algorithm solves SAT faster than roughly $O(2^n \cdot \text{poly}(n))$ in the worst case (modern SAT solvers do vastly better in practice via heuristics, but no worst-case polynomial bound is known or believed to exist). ``` Brute-Force-SAT(φ):

# φ is a CNF formula over variables x_1,...,x_n for each of the 2^n assignments a to x_1,...,x_n: if Verify-SAT(φ, a): return "satisfiable", a return "unsatisfiable" ```

Reducing SAT to 3-SAT. To show 3-SAT is NP-complete via SAT (rather than directly via the Cook-Levin construction), one gives a polynomial-time transformation converting any CNF clause into an equisatisfiable conjunction of 3-literal clauses:

• A clause with 1 literal $(\ell_1)$: introduce two fresh variables $p, q$ and replace it with

$(\ell_1 \lor p \lor q)\land(\ell_1 \lor \lnot p \lor q)\land(\ell_1 \lor p \lor \lnot q)\land(\ell_1 \lor \lnot p \lor \lnot q)$.

• A clause with 2 literals $(\ell_1 \lor \ell_2)$: introduce fresh $p$, replace with $(\ell_1\lor \ell_2\lor p)\land(\ell_1\lor\ell_2\lor\lnot p)$.
• A clause with exactly 3 literals: keep as is.
• A clause with $k>3$ literals $(\ell_1\lor\ell_2\lor\cdots\lor\ell_k)$: introduce $k-3$ fresh variables $z_1,\dots,z_{k-3}$ and chain them:

``` CNF-to-3CNF(φ): ψ ← empty conjunction for each clause C in φ: k ← number of literals in C if k == 3: append C to ψ else if k == 1: introduce fresh p, q append the four 3-literal clauses expanding (ℓ1) as above else if k == 2: introduce fresh p append the two 3-literal clauses expanding (ℓ1 ∨ ℓ2) else: # k > 3 introduce fresh z_1,...,z_{k-3} append the chain of (k-2) 3-literal clauses linking z_1..z_{k-3} return ψ ``` Each new clause introduces at most a constant number of fresh variables and clauses per original clause, so $|\psi| = O(|\varphi|)$ and the whole transformation runs in polynomial (indeed linear) time. The key correctness claim — the chain clause is satisfiable exactly when the original long clause is — is verified below.

Membership in NP. For both SAT and 3-SAT, a satisfying assignment is a certificate of size $O(n)$ bits. `Verify-SAT` checks it in $O(m \cdot k)$ time where $k$ is the maximum clause length (a fixed constant, 3, for 3-SAT; bounded by formula length in general). Since verification is polynomial in the input size, both problems are in NP by definition.

NP-hardness (sketch, formalized by Cook-Levin). The Cook-Levin theorem shows that for any language $L \in \mathrm{NP}$, decided by a nondeterministic Turing machine $N$ running in time $p(n)$ for polynomial $p$, one can build — in time polynomial in $n$ — a CNF formula $\varphi_w$ (for input $w$) such that

The construction encodes the entire computation history (a tableau: one row per time step, one cell per tape position) as Boolean variables, with clauses enforcing (1) each cell holds exactly one symbol, (2) the machine starts in the correct initial configuration, (3) each configuration follows validly from the previous one according to $N$'s transition function, and (4) some row reaches an accepting state. Because $N$ runs in time $p(n)$, the tableau has $O(p(n)^2)$ cells (each of the $p(n)$ steps can move the head by at most 1, so the tape used is $O(p(n))$), giving polynomially many variables and clauses — the reduction is polynomial-time. This article treats the theorem as a black box; the Cook-Levin Theorem entry gives the full tableau construction.

Correctness of the SAT-to-3SAT reduction. We must verify that `CNF-to-3CNF` preserves satisfiability. The 1-literal and 2-literal clause expansions are easily checked by truth table: e.g. for $(\ell_1)$, the four-clause expansion is satisfiable under any assignment of $p,q$ precisely when $\ell_1$ is TRUE (if $\ell_1$ is FALSE, the four clauses collectively demand all four combinations of $(p,q)$ be excluded, an unsatisfiable set; if $\ell_1$ is TRUE every clause is automatically satisfied regardless of $p,q$). For the long-clause chain, the key invariant is: > Claim. $(\ell_1\lor\cdots\lor\ell_k)$ is satisfiable under assignment $a$ to the original variables iff the chain of 3-literal clauses (with fresh $z_1,\dots,z_{k-3}$) is satisfiable by extending $a$ with some assignment to the $z_i$. Proof. ($\Rightarrow$) Suppose some $\ell_j$ is TRUE under $a$. Set $z_i = \text{TRUE}$ for all $i < j-1$ and $z_i = \text{FALSE}$ for all $i \ge j - 1$ (informally: "$z_i$ true" means "satisfied by one of $\ell_1,\dots,\ell_{i+2}$"). Each chain clause then contains either a true $\ell$ literal or a true/false pairing of consecutive $z$'s that satisfies it — a direct case check confirms every clause in the chain holds. ($\Leftarrow$) Conversely, suppose no $\ell_j$ is TRUE. Then the first clause $(\ell_1\lor\ell_2\lor z_1)$ forces $z_1 = \text{TRUE}$. Each subsequent clause $(\lnot z_{i-1}\lor \ell_{i+1}\lor z_i)$, with $\ell_{i+1}$ false and $z_{i-1}$ true, forces $z_i = \text{TRUE}$ by resolution. This propagates until the last clause $(\lnot z_{k-3}\lor \ell_{k-1}\lor \ell_k)$, which with $z_{k-3}=\text{TRUE}$ and $\ell_{k-1},\ell_k$ false is FALSE — contradiction. Hence if no original literal is true, the chain is unsatisfiable. $\blacksquare$ Since satisfiability is preserved in both directions and the transformation size is linear, 3-SAT is NP-hard; combined with membership in NP, 3-SAT is NP-complete.

Complexity summary.

The honest tradeoff: while worst-case SAT solving is exponential, modern conflict-driven clause learning (CDCL) solvers routinely solve industrial instances with millions of variables in seconds — because real instances have exploitable structure absent in adversarial worst-case formulas. Theoretical hardness (worst-case, assuming P ≠ NP) and practical solvability (average-case, structured instances) are not contradictions; they describe different regimes.

Consider the CNF formula over variables $x_1, x_2, x_3$:

This has one 2-literal clause, so it is not already 3-CNF. Let's first solve it directly by brute force, then show the 3-CNF conversion of the offending clause.

Brute-force search over $2^3 = 8$ assignments:

Only the assignment $x_1{=}0, x_2{=}0, x_3{=}1$ satisfies all four clauses, so $\varphi$ is satisfiable, and `Brute-Force-SAT` returns this assignment after checking (in the worst case) all 8 rows.

Converting $C_2 = (\lnot x_1 \lor x_2)$ to 3-CNF. It has 2 literals, so introduce a fresh variable $p$ and replace $C_2$ with:

Check the invariant on our satisfying assignment: $x_1 = 0, x_2 = 0$ makes $\lnot x_1 = 1$, so both new clauses are TRUE regardless of $p$ — consistent with $C_2$ being TRUE under this assignment for any value of $p$. If instead $x_1 = 1, x_2 = 0$ (making original $C_2$ false), then $\lnot x_1 = 0, x_2 = 0$, so both clauses reduce to $(0\lor 0\lor p)=p$ and $(0\lor 0\lor \lnot p)=\lnot p$ — together these force $p \land \lnot p$, an unsatisfiable pair, exactly mirroring that $C_2$ cannot be satisfied. The transformation is confirmed correct on this instance.

SAT solvers are deployed as general-purpose combinatorial engines across engineering. Hardware verification teams at chip manufacturers use SAT solvers to formally check that circuit designs match specifications, encoding equivalence checking as a satisfiability query. Software verification and bug-finding tools (symbolic execution engines, bounded model checkers) translate program paths into SAT or SMT (SAT-modulo-theories) instances to detect buffer overflows and assertion violations. AI planning and scheduling systems encode "does a valid plan of length $k$ exist" as SAT and call off-the-shelf solvers rather than write bespoke search code. Package managers (resolving mutually compatible software versions) and cryptanalysis (encoding cipher-breaking as SAT) are further practical uses. Theoretically, SAT and 3-SAT are the seed of essentially all of NP-completeness theory: the Cook-Levin Theorem establishes SAT's hardness from first principles, and 3-SAT is the standard reduction source used to establish hardness for graph problems like those in Classic NP-Complete Problems: Clique and Vertex Cover, as well as for scheduling, packing, and countless other combinatorial problems throughout NP-Completeness theory.

Ask the tutor: How exactly does the Cook-Levin tableau construction encode a Turing machine's transition function as CNF clauses?