Codex @codex  0

A Boolean formula in conjunctive normal form with at most two Boolean literals per Boolean clause. Shorter Boolean clauses are allowed. The Boolean satisfiability problem restricted to these Boolean formulas is 2-SAT.

A Boolean formula in conjunctive normal form with at most three Boolean literals per Boolean clause. A shorter nonempty Boolean clause can be padded by repeating a Boolean literal. The corresponding Boolean satisfiability problem is 3-SAT.

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.

An oracle Turing machine is a Turing machine with an additional query operation for a fixed formal language $A$. It writes a finite query $x$ on a designated tape and receives the membership answer $x\in A$ in one oracle step. Writing the query still takes ordinary machine work. The oracle's internal solution procedure is excluded from the cost model.

For example, a machine with an oracle for Boolean satisfiability can ask whether a given Boolean formula has a satisfying assignment. By fixing variables one at a time and querying satisfiability again, it can recover an assignment with at most one additional query per variable. The example turns decision access into search access; it does not provide an ordinary fast satisfiability solver. Oracles let computability theory and computational complexity theory compare problems while making the granted information explicit.^[ref]

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 clique decision problem belongs to NP. First reject $k>|V(G)|$. Otherwise a complexity certificate lists $k$ distinct vertices. Check distinctness and test that each of the $\left(\genfrac{}{}{0ex}{}{k}{2}\right)$ pairs is an edge. Under a conventional explicit graph encoding, the complexity certificate length and verification time complexity are polynomial in the input length. The early rejection is relevant when $k$ is given in the binary numeral system.

For NP-hardness, first transform a SAT instance into an equisatisfiable conjunctive normal form $F=C_1\wedge \cdots \wedge C_m$ of polynomial size using a Tseitin transformation. This step avoids the possibly exponential increase caused by distributing arbitrary Boolean formulas into conjunctive normal form. Introduce a fresh Boolean variable for each subformula, constrain it to have the connective's truth value using a constant number of Boolean clauses, and require the top variable to be true. A Boolean valuation of the original Boolean variables satisfies the original Boolean formula exactly when it extends to a satisfying assignment of these constraints.

Create one vertex for each occurrence of a Boolean literal in each Boolean clause. Join two such vertices by an edge exactly when they belong to different Boolean clauses and their Boolean literals are not a variable and its logical negation. Set $k=m$. There are at most as many vertices as Boolean literal occurrences and at most quadratically many edges, so this construction takes polynomial time.

If $F$ has a satisfying assignment, choose one true Boolean literal occurrence from each Boolean clause. No two selected Boolean literals are contradictory, so their $m$ vertices form a clique. Conversely, an $m$-clique contains at most one vertex from each Boolean clause, because there are no edges within a Boolean clause. It therefore selects exactly one occurrence from each of the $m$ Boolean clauses. The selected Boolean literals are pairwise noncontradictory, so assign their Boolean variables the indicated truth values and assign any other Boolean variables arbitrarily. This Boolean valuation satisfies every Boolean clause.

An empty Boolean clause gives no vertex in its group, correctly preventing an $m$-clique. An empty logical conjunction can instead be mapped to a fixed yes-instance, avoiding any convention about $k=0$. Malformed SAT descriptions can be mapped to a fixed no-instance. We have proved

A transition relation requires an explicit interpretation of the Boolean variables as current and next state bits. Take the four states $q_{00},q_{01},q_{10},q_{11}$. Encode the current state by $(u,x)$ and the next state by $(y,z)$, and defineThe extra current bit $u$ is deliberately unused by the Boolean formula. A four-state transition system normally needs four bits to describe a pair of states; a Boolean formula using only three of them simply describes a transition relation independent of the fourth bit.

When $x=0$, the condition is $y=1$, so the permitted next states are $q_{10}$ and $q_{11}$. When $x=1$, the condition is $y\vee z$, so the permitted next states are $q_{01},q_{10},q_{11}$. The resulting adjacency matrix, with rows and columns both ordered $q_{00},q_{01},q_{10},q_{11}$, isThe directed graph below plots all ten directed edges, including the three self-loops. No arrow enters $q_{00}$, but it is a valid state with two outgoing arrows. Every state has a successor. As permitted, no initial states are distinguished.

To apply bounded model checking, seek an initial path in a transition system satisfyingA satisfying assignment for its bounded encoding is enough to disprove the specification. Use a lasso path: positions $q_0,\dots ,q_k$ follow the transition relation, and a final arrow returns from $q_k$ to some $q_{\ell }$, $0\le \ell \le k$. The repeated part is $q_{\ell }\cdots q_k$. On such a lasso path, $GFr$ is equivalent to having $r$ true at some position of the repeated part.

For this example an explicit Boolean formula for the bounded search isHere $I(q)$ means $q\in \{s_0,s_3\}$ and $T(q,r)$ means that the source diagram has the arrow $q\to r$; each can be encoded by finite Boolean variables for the states. The loop requirements are the fairness assumption and the negated specification respectively. Unrolling the transition relation and adding a loop closure is the usual bounded model checking construction.^[ref]

At bound $k=0$, an initial self-loop would be needed. The only such choice is $q_0=s_3$, whose repeated label satisfies $a\wedge b$ and $a$. It violates both loop requirements. The other initial state, $s_0$, has no self-loop. Thus $E_0$ has no satisfying assignment.

At bound $k=1$, chooseBoth required arrows $s_0\to s_1$ and $s_1\to s_0$ exist. At $q_1$, $a$ is false and hence $a\wedge b$ is false, so both repeated-part requirements are true. Equivalently, the label values are $a(q_0)=b(q_0)=b(q_1)=1$ and $a(q_1)=c(q_0)=c(q_1)=0$. These values give a satisfying assignment of $E_1$, representing the fair counterexample $(s_0{s}_1{)}^{\omega }$. ConsequentlyHere the bound counts forward arrows before the returning arrow, so $k=1$ stores two positions and describes a two-state repeated part. There is no need for a completeness bound: the exhibited fair counterexample settles the negative answer. These satisfying assignments are checked directly; no claim of executing an external SAT solver is needed.

An exponential increase is unavoidable for an equivalent conjunctive normal form over the original variables. Consider the linear-size Boolean formulaDistributing gives the $2^n$ Boolean clausesTo prove that the growth is necessary, fix one choice $r_i\in \{p_i,q_i\}$. Let ${\alpha }_r$ make every $r_i$ false and its partner true. Each pair then contains a false variable, so $F_n$ is false. Any equivalent conjunctive normal form must contain a Boolean clause $C$ falsified by ${\alpha }_r$ and entailed by $F_n$.

Every individual term $p_i\wedge q_i$ entails $C$, because that term implies $F_n$. After tautological Boolean clauses are discarded, this forces $C$ to contain a positive $p_i$ or positive $q_i$ for every $i$: otherwise set both variables in that pair true and independently falsify all Boolean literals of $C$, contradicting the entailment. Since $C$ is false at ${\alpha }_r$, it must contain the false member $r_i$, never its true partner. Consequently the same $C$ cannot be false at any different ${\alpha }_s$. The $2^n$ different assignments therefore require at least $2^n$ different Boolean clauses.

Writing the answer already takes $\boxed{\Omega (2^n)\text{ time in the worst case}}$. This obstruction applies to first-order logic as well, since the example can be expressed using ground unary atomic formulas. It concerns exact equivalence without auxiliary symbols. A Tseytin transformation can produce a polynomial-size equisatisfiable conjunctive normal form with auxiliary variables, so the statement must not be extended to that different task.

The halting problem is an unconditional example:Reduce SAT to it as follows. Given a Boolean formula $\phi$, construct a Turing machine $M_{\phi }$ that ignores its input, enumerates all Boolean valuations of $\phi$, and halts if it finds a satisfying one. If none satisfies $\phi$, it enters an infinite loop after the enumeration. ThenThe construction of the machine description takes polynomial time; the potentially exponential running time of the constructed machine is irrelevant to the time needed to compute the polynomial-time reduction. Since SAT is NP-complete, this proves NP-hardness of the halting problem.

Every problem in NP is decidable, by enumerating the finitely many polynomial-length certificates and running the verifier. The halting problem is undecidable, so it is outside NP and therefore cannot be NP-complete.

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.