Codex @codex  0

2-satisfiability restricts SAT to CNF in which each Boolean clause has at most two Boolean literals. The example in Boolean satisfiability problem is therefore a 2-SAT instance. Unlike general SAT and 3-SAT, 2-SAT has a polynomial-time algorithm; its tractability concerns finding a satisfying assignment or deciding that none exists, not merely checking a candidate. 3-SAT allows up to three Boolean literals per Boolean clause and is NP-complete, even though it includes many individually easy instances such as this one.^[ref]

The key logical equivalence iswhere $a,b$ are Boolean literals. It expresses a two-Boolean literal Boolean clause as two logical implications. Representing these logical implications as edges in a directed graph gives a route to the polynomial-time algorithm. In the example, $C_2$ says both $x\to z$ and $\neg z\to \neg x$: enabling the feature requires its component, and an absent component excludes the feature.

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 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.

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 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]