= Boolean satisfiability problem
{c}
{wiki}
= SAT
{c}
{synonym}
= Boolean satisfiability
{c}
{synonym}
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>, write
$$
F=C_1\land\cdots\land C_m,
\qquad C_i=\ell_{i1}\lor\cdots\lor\ell_{ik_i}.
$$
Each <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> example
$$
F=(x\lor y)\land(\neg x\lor z)\land(\neg y\lor\neg z),
\qquad C_1=x\lor y,\quad C_2=\neg x\lor z,\quad C_3=\neg y\lor\neg z.
$$
At 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>.
\Image[/satisfiability-assignment-clause-evaluation.png]
{title=An original <satisfying assignment> evaluated through <Boolean literals>, three <Boolean clauses>, and their <logical conjunction>}
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>.
\Image[/satisfiability-eight-assignment-truth-table.png]
{title=All eight <Boolean valuations> of the original <CNF> example, with its two <satisfying assignments> highlighted}
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>.<The Complexity of Theorem-Proving Procedures by Stephen A. Cook>[The Complexity of Theorem-Proving Procedures by Stephen A. Cook, 1971, §1, Theorem 1 and proof, pp. 2–3 of the revision-3 transcription: CNF encodes accepting computations]{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\lor z$; <De Morgan's laws> rewrite the third rule $\neg(y\land z)$ as $\neg y\lor\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.
Back to article page
