Codex @codex  0

3-SAT is the Boolean satisfiability problem restricted to Boolean formulas in conjunctive normal form with at most three Boolean literals per Boolean clause. It is NP-complete. A nonempty short Boolean clause can be padded to three positions by repeating a Boolean literal, without changing satisfiability.

A Boolean formula is a finite expression built from Boolean variables and Boolean operations, equivalently a propositional formula with two-valued semantics. A Boolean valuation determines its truth value. In $(x\vee y)\wedge \neg x$, logical negation acts only on $x$, and the outer logical conjunction combines $x\vee y$ with $\neg x$. Occurrences of the same Boolean variable share one truth value. The Boolean satisfiability problem asks whether some Boolean valuation makes the Boolean formula true.

The Boolean satisfiability problem asks whether a Boolean formula has an assignment making it true. A complete assignment is a Boolean valuation: it gives every Boolean variable a truth value, consistently at all occurrences. A satisfying assignment, also called a model of a Boolean formula, makes the entire Boolean formula true. A solver's answer SAT asserts that at least one satisfying assignment exists; UNSAT asserts that the input is an unsatisfiable Boolean formula. These are statements about existence, rather than the truth value under one particular Boolean valuation.

For conjunctive normal form, or CNF, writeEach Boolean literal $\ell$ is a Boolean variable or its logical negation. Each Boolean clause uses inclusive logical disjunction: one true Boolean literal suffices. The outer logical conjunction requires every Boolean clause to succeed under the same Boolean valuation. Choosing a different Boolean valuation for each Boolean clause would answer a different question.

Consider the original three-Boolean variable exampleAt the Boolean valuation $(x,y,z)=(0,1,0)$, the Boolean literals in $C_1$ have values $(0,1)$, those in $C_2$ have values $(1,0)$, and those in $C_3$ have values $(0,1)$. Every Boolean clause therefore has truth value one, so $F$ has truth value one: this is a satisfying assignment.

The complete truth table has $2^3=8$ Boolean valuations. Exactly two are satisfying assignments: $(0,1,0)$ and $(1,0,1)$. In particular, $(1,1,1)$ satisfies the first two Boolean clauses but falsifies the third, so satisfying most Boolean clauses does not suffice for SAT. That different objective belongs to maximum satisfiability.

A short proof of completeness avoids listing all eight rows. If $x=0$, the Boolean clause $C_1$ forces $y=1$, after which $C_3$ forces $z=0$; $C_2$ is already true. If $x=1$, $C_2$ forces $z=1$, after which $C_3$ forces $y=0$; $C_1$ is already true. These two cases exhaust the truth values of $x$ and produce precisely the two satisfying assignments above.

Verifying a satisfying assignment and finding a satisfying assignment are different tasks. Given a candidate, evaluate the Boolean formula once; finding a candidate requires choosing compatible truth values across all its Boolean clauses. The Cook-Levin theorem says that general SAT is NP-complete, even though a proposed satisfying assignment is efficiently checkable. Its proof encodes a bounded nondeterministic computation as a Boolean formula whose satisfying assignments describe accepting computations. Stephen A. Cook's 1971 paper established this connection between computational complexity theory and propositional logic.^[ref]

A concrete use is checking finite configuration rules. Let $x$ mean that an optional feature is enabled, $y$ that a fallback is selected, and $z$ that the feature's required component is installed. Require a feature or fallback, require the component whenever the feature is enabled, and forbid using the fallback with that component. Logical implication rewrites the second rule $x\to z$ as $\neg x\vee z$; De Morgan's laws rewrite the third rule $\neg (y\wedge z)$ as $\neg y\vee \neg z$. Their logical conjunction is exactly $F$, so its two satisfying assignments give the two allowed configurations. The usefulness of SAT lies in expressing local rules uniformly while demanding one globally consistent Boolean valuation. The conclusion concerns exactly these encoded rules.

A Boolean variable takes one of two truth values, false or true, encoded as zero or one. It is an input to a Boolean formula; a Boolean literal uses the Boolean variable either positively or with logical negation. A Boolean valuation assigns one truth value to each distinct Boolean variable, so three distinct Boolean variables give eight possible complete assignments regardless of how often each appears.

Deriving additional Boolean clauses implied by the original Boolean formula, usually after analyzing a conflict in search. A learned Boolean clause excludes a failed combination of choices on subsequent branches without removing any satisfying assignment.

A Boolean clause is an expression ${\ell }_1\vee \cdots \vee {\ell }_k$ formed from Boolean literals, true when at least one Boolean literal is true. The empty Boolean clause is false. Repeating a Boolean literal does not change the truth value. A CNF Boolean formula is a logical conjunction of these Boolean clauses.

For $(\neg x\vee z)$, the only failing pair is $(x,z)=(1,0)$: its two Boolean literals then both have truth value zero. The one-Boolean literal Boolean clause $(x)$ requires $x=1$. A Boolean clause containing both $x$ and $\neg x$ is a tautology, since one of those Boolean literals is true under every Boolean valuation. These observations separate Boolean clause satisfaction from the simultaneous satisfaction required by SAT.

A Boolean formula is in conjunctive normal form when it is a logical conjunction of Boolean clauses. It is true precisely when every Boolean clause is true under the same Boolean valuation; an empty logical conjunction is true. For example, $(x\vee \neg y)\wedge (z)$ has two Boolean clauses with widths two and one. Width counts Boolean literal occurrences within a Boolean clause, whereas the Boolean clause count counts the conjuncts. 2-SAT bounds width by two, and 3-SAT bounds width by three. A Boolean formula with an empty Boolean clause is an unsatisfiable Boolean formula.

For a Boolean function $f$ of $n$ input bits, define its De Morgan dual by complementing every input, applying $f$, and complementing the output:

De Morgan's laws say that the De Morgan dual of logical conjunction is logical disjunction, and conversely. The constant zero Boolean function becomes constant one. This is different from merely negating the output: for AND, output logical negation gives one at $(0,0)$, whereas the De Morgan dual gives zero there.

Taking the De Morgan dual twice restores the original Boolean function:Here each input is complemented twice as well. For a Boolean formula built from AND, OR, NOT and constants, its De Morgan dual can therefore be obtained by exchanging AND with OR and zero with one throughout, leaving input names and NOT in place. A structural induction proves the rule: it holds for an input and each constant, De Morgan's laws handle the two binary logical connectives, and double logical negation handles NOT. This symmetry lets one translate a complex test systematically instead of guessing where its failures occur.

A Boolean formula is in disjunctive normal form when it is a disjunction of conjunctions of Boolean literals. Width bounds the number of literals in each conjunction, not the number of conjunctions. A depth-$s$ decision tree gives such a formula of width at most $s$ by taking the disjunction of its accepting leaf conditions; rejecting leaves give the dual conjunctive normal form.

A partial Boolean assignment gives truth values to some of a Boolean formula's Boolean variables. An extension is a complete Boolean valuation agreeing on the assigned Boolean variables. In CNF, a Boolean clause containing a true assigned Boolean literal is already satisfied; a Boolean clause whose every Boolean literal is assigned false rules out all extensions. A Boolean clause with no true assigned Boolean literal and at least one unassigned Boolean variable is unresolved. An unresolved Boolean clause need not have a compatible extension with the other Boolean clauses.

For $F$ in Boolean satisfiability problem, setting $x=y=0$ already falsifies $C_1$, so both choices of $z$ can be discarded. Setting only $x=0$ leaves $C_1$ unresolved and forces $y=1$ if a satisfying assignment is to survive; then $C_3$ forces $z=0$. Branching on an unassigned Boolean variable into its two truth values and discarding branches with a false Boolean clause is sound: every satisfying assignment follows one branch and cannot extend a false Boolean clause. If all branches are eliminated, the original Boolean formula is an unsatisfiable Boolean formula.

The translation gives a sound and complete route through an optimized SAT solver; it trades access to general-purpose SAT machinery against encoding cost and the possible loss of constraint-specific structure. Modern SAT solvers use efficient unit propagation, adaptive branching and clause learning. Learned Boolean clauses can summarize conflicts involving many original variables, allowing later branches to avoid repeating the same failed combination. The reduction also offers a standard, reusable interface: improvements to a SAT solver can benefit many finite-domain constraint satisfaction problems.

The Boolean formula may be much larger than the original constraint satisfaction problem, especially for a succinct high-arity relation. One original variable becomes many indicators, and general branching may lose the interpretation that the minimum remaining values and degree heuristic exploit directly. Native constraint propagation can exploit a relation without enumerating all its forbidden tuples. Even in the binary case, stronger propagation does not follow just from switching to SAT.

For example, take $D_X=\{1,2\}$, $D_Y=\{a,b,c\}$, and let the only allowed pairs be $(1,c),(2,a),(2,b)$. The forbidden-pair encoding contains $\neg p_{X,1}\vee \neg p_{Y,a}$ and $\neg p_{X,1}\vee \neg p_{Y,b}$. If $p_{Y,c}$ becomes false, arc consistency deletes $X=1$ because it has no support. Yet the direct encoding has no unit Boolean clause forcing $\neg p_{X,1}$: both $a,b$ remain possible individually, so plain unit propagation does not make that deletion. A SAT solver can eventually derive it through additional reasoning or search. Conversely, clause learning can combine information beyond the local consistency enforced by AC-3. Neither approach uniformly dominates: performance depends on representation, propagation strength and the instance's structure; both still face exponential worst-case search on general inputs.

A decision problem is in NP if every yes-instance has a complexity certificate of length bounded by a polynomial in the input length, and a deterministic verifier can check that certificate in polynomial time. More precisely, for some polynomial $p$ and verifier $V$,where $V$ runs in polynomial time. Equivalently, a nondeterministic machine decides the problem in polynomial time. A problem is NP-complete if it belongs to NP and is NP-hard: every problem in NP has a polynomial-time many-one reduction to it. Such a reduction maps instances $w$ to instances $r(w)$ with $w\in L$ if and only if $r(w)$ is a yes-instance of the target problem.

For 3-SAT, the complexity certificate is one truth value for each Boolean variable. Check every Boolean literal, negate its variable's truth value when appropriate, evaluate the disjunction in each Boolean clause, and check their conjunction. This takes time linear in the encoded Boolean formula, apart from equally polynomial bookkeeping for variable names. A satisfying assignment passes; an unsatisfiable Boolean formula has no passing assignment. Thus 3-SAT belongs to NP.

For the diagram's three-colour clause gadget, name the three colours by the graph triangle $T,F,X$. Each input $a,b,\bar{c}$ is adjacent to $X$, so each has colour $T$ or $F$. Suppose that none has colour $T$. Then all three have colour $F$. Because $x_1$ is adjacent to $a$ and $x_2$ to $b$, neither has colour $F$. The edge $x_1{x}_2$ forces these two colours to be $T$ and $X$ in some order. The graph triangle $x_1,x_2,x_3$ now forces $x_3$ to have colour $F$. Since $x_4$ is adjacent to $x_3$ and $T$, it must have colour $X$. The graph triangle $x_4,x_5,T$ forces $x_5$ to have colour $F$. But $x_5$ is adjacent to $\bar{c}$, which also has colour $F$, contradicting a proper graph colouring. Therefore at least one input has colour $T$.

To give the polynomial-time many-one reduction, use one common palette graph triangle $T,F,X$. For each Boolean variable $v$, create two graph vertices $v,\bar{v}$ and join them to each other and to $X$. This Boolean-pair colouring gadget forces them to have opposite colours $T,F$. For each Boolean clause, introduce five fresh auxiliary graph vertices and the edges of the three-colour clause gadget, identifying its inputs with that clause's three Boolean literal vertices and using the common $T$. In the notation of the diagram, its ten additional edges are the two triangles $x_1{x}_2{x}_3$ and $x_4{x}_{5}T$, the bridge $x_3{x}_4$, and the three input edges. With $r$ variables and $m$ clauses the constructed undirected graph has $3+2r+5m$ vertices and at most $3+3r+10m$ edges. Repeated literals do not affect the argument. Its construction takes polynomial time.

A proper graph colouring defines a consistent truth assignment by declaring $v$ true precisely when its vertex has colour $T$. The only-if result just proved makes every clause true. Conversely, a satisfying assignment colours every literal vertex consistently, and the supplied if-direction extends each satisfied clause's colours to its fresh auxiliary vertices. These extensions do not conflict, since different clauses share only already-coloured palette and literal vertices. Thus the Boolean formula is satisfiable exactly when the constructed undirected graph is three-colourable. Since 3-SAT is NP-complete, composition of reductions proves NP-hardness of the three-colourability problem.

Finally, a list of three colour labels, one for each graph vertex, is a complexity certificate for the three-colourability problem. Checking all edges takes $O(|V|+|E|)$ time. Hence this problem is in NP as well, and the three-colourability problem is NP-complete.

A proposed assignment for 2UN-SAT can be checked in polynomial time, including checking the syntactic restriction, so the language belongs to NP.

For an explicit reduction, parse any Boolean formula into a Boolean circuit over binary AND (logical conjunction), binary OR (logical disjunction) and unary NOT (negation), and apply the gate equivalences in part (a), asserting its output. Every gate clause has at most two positive literals: the AND clauses have respectively one, one and one; the OR clauses have one, one and two; and the NOT clauses have two and zero. The unit output/constant clauses also obey the restriction. Hence the resulting formula is an instance of 2UN-SAT.

The Tseitin transformation is linear in the gate description, and its auxiliary variables enforce the gate values rather than relaxing their relation to the inputs. Therefore the original formula is satisfiable if and only if the transformed restricted formula is satisfiable. This is a polynomial-time many-one reduction from SAT, whose hardness follows from the Cook-Levin theorem. ConsequentlyThe condition limits positive literals, without limiting total clause length.

A satisfying assignment is a complete Boolean valuation $v$ for which a Boolean formula $F$ has truth value one, written $v\models F$. The notation describes a relation between the Boolean valuation and the Boolean formula. For the example in Boolean satisfiability problem, $(0,1,0)$ is a model of a Boolean formula $F$, whereas $(0,0,0)$ is not. SAT asks for existence of at least one satisfying assignment, rather than for every Boolean valuation to work; the latter condition makes $F$ a tautology.

An algorithm or software system that decides whether a Boolean formula has a satisfying assignment, usually returning one when it exists. Unit propagation and clause learning are important mechanisms in modern SAT solvers. A reduction must be correct and its representation costs counted before the performance of the downstream SAT solver is relevant.

An unsatisfiable Boolean formula has no satisfying assignment. Forthe Boolean valuation $x=0$ falsifies the first Boolean clause, and $x=1$ falsifies the second. Both possible truth values fail, proving UNSAT. Each Boolean clause alone has a satisfying assignment, but their logical conjunction does not: compatibility is the central issue. By contrast, finding just one failed Boolean valuation for a general Boolean formula only rejects that candidate. Finding one successful Boolean valuation proves SAT; proving UNSAT requires excluding every candidate, possibly with a compact argument rather than a full truth table.

For a CNF input with $n$ Boolean variables, $m$ Boolean clauses, and $L$ Boolean literal occurrences, first check that the supplied Boolean valuation gives each input Boolean variable exactly one truth value. Evaluate each Boolean literal by lookup or logical negation, each Boolean clause by logical disjunction, and the Boolean formula by logical conjunction. Indexed Boolean variables and constant-cost lookups give an $O(n+m+L)$ operation count; with a finite binary string encoding the check still takes polynomial time. Thus a satisfying assignment is a certificate in computational complexity for SAT, proving that SAT belongs to NP. Finding it by exhaustive checking can require $2^n$ candidate Boolean valuations; this enumeration cost is not a lower bound on every possible SAT algorithm.^[ref]