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.

Approximate quantum counting estimates the number $k$ of satisfying assignments of a Boolean function, using a quantum oracle and quantum measurement. Controlled repetitions of a Grover search algorithm iteration let quantum interference reveal the count. For one input bit, a Hadamard test can give Pauli Z gate expectation value $1-k$: with the complemented phase oracle $U_f=\mathrm{diag}(2f(0)-1,2f(1)-1)$ and $G=-X{U}_f$, use $⟨+|X=⟨+|$ to obtain $⟨+|G|+⟩=-[(2f(0)-1)+(2f(1)-1)]/2=1-k$. Repeated preparations estimate this expectation value; one binary measurement result does not distinguish all three counts $0,1,2$.

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 formal verification method that encodes a bounded execution and a violated specification as a Boolean satisfiability problem. A satisfying assignment yields a counterexample. For infinite-path properties, a lasso path can finitely represent a repeated execution. Failure to find a counterexample at one finite bound alone does not prove an unbounded property.^[ref]

Given a succinct Boolean game and a complete pure strategy strategy profile, determine whether it is a Nash equilibrium. The problem is co-NP-complete for goal propositional formulas, even with one player. This differs from existential equilibrium checking in a Boolean game, which searches for some qualifying Nash equilibrium.

A negative instance has a short complexity certificate: a currently unsatisfied player and new truth values for that player's controlled Boolean variables that make the goal true. Evaluating the current and changed propositional formulas takes polynomial time, proving membership in co-NP.

For hardness, given a propositional formula $F(X)$, let one player control $X$ and a fresh variable $z$, with goal $z\wedge F(X)$. The all-false candidate has payoff zero. It is a Nash equilibrium exactly when $F$ is an unsatisfiable Boolean formula, since any satisfying assignment permits an improvement by also setting $z$ true. This is a polynomial-time many-one reduction from unsatisfiability. The fresh guard ensures that the candidate loses independently of the input formula's value there.

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.

Given an explicitly represented finite simple graph $G$ and a nonnegative integer $k$, decide whether $G$ contains a clique of size $k$. The problem is NP-complete. A polynomial-time many-one reduction from SAT first obtains conjunctive normal form by a Tseitin transformation, makes one vertex per Boolean literal occurrence, and joins noncontradictory occurrences from different Boolean clauses. A clique as large as the Boolean clause count is equivalent to a satisfying assignment.

Represent each original value choice $X_i=v$ by a Boolean variable $p_{i,v}$ and impose an exactly-one constraint for each original variable. For every forbidden tuple $(v_i{)}_{i\in S}$ of a constraint with scope $S$, add the Boolean clause ${\bigvee }_{i\in S}\neg p_{i,v_i}$. A complete original assignment satisfies every constraint exactly when its one-hot indicators satisfy all these Boolean clauses: each forbidden-tuple Boolean clause excludes precisely that joint choice. A satisfying assignment decodes by reading the unique true indicator for each original variable.

For constraint domain sizes $q_i$, pairwise uniqueness requires ${\sum }_i\left(\genfrac{}{}{0ex}{}{q_i}{2}\right)$ Boolean clauses. If a constraint has $f_C$ forbidden tuples and arity $r_C$, its contribution is $f_C$ Boolean clauses and $r_C{f}_C$ literal occurrences. Thus bounded arity gives a polynomial-size encoding in explicitly listed domains, whereas enumerating a succinct high-arity relation can be exponential in its description length. Unit propagation on this encoding can be weaker than arc consistency on the original binary constraints.

The Horn-SAT forward-chaining algorithm maintains the set $T$ of Boolean variables already forced true. Write each Horn clause as an implication $a_1\wedge \cdots \wedge a_k\to b$, where the conclusion is either a Boolean variable or false. Start with $T=\varnothing$. Whenever every antecedent belongs to $T$, add the conclusion $b$; if the conclusion is false, report failure.

Every satisfying assignment must make all members of $T$ true: this holds initially and is preserved by each enabled implication. Thus an enabled false conclusion proves that no satisfying assignment exists. If no further Boolean variable can be added and no such failure occurs, interpreting exactly $T$ as true satisfies every Horn clause. It is the least satisfying assignment under inclusion of true Boolean variables.

For example, the clauses $p$, $p\to q$ and $q\to r$ force $T=\{p,q,r\}$. Adding $r\to \mathrm{false}$ makes the instance unsatisfiable. Each Boolean variable enters $T$ at most once. Indexing antecedent occurrences and maintaining a counter per clause permits one update per occurrence, avoiding repeated full scans.

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

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.

Use an exactly-one constraint for each finite-domain variable and a Boolean clause forbidding each disallowed constraint tuple. Let the variables be $X_1,\dots ,X_n$, with explicitly listed finite constraint domains $D_i$, and let constraint $C$ have distinct-variable scope $S_C$ and allowed relation $R_C\subseteq {\prod }_{i\in S_C}{D}_i$. Introduce a Boolean variable $p_{i,v}$ for every $v\in D_i$, interpreted as $X_i=v$. The direct SAT encoding of finite-domain constraints isIn the middle logical conjunction, each unordered distinct pair is included once. The first Boolean clause requires at least one value, the pairwise Boolean clauses permit at most one, and a final Boolean clause is false exactly when all coordinates of one forbidden tuple are selected. The formula is in conjunctive normal form. An empty constraint domain produces an empty Boolean clause, correctly making the instance unsatisfiable.

For soundness of the reduction, a solution $x$ of the constraint satisfaction problem gives the Boolean valuation $p_{i,v}=1$ exactly when $v=x_i$. Every exactly-one constraint holds; a forbidden tuple differs from $x$ on at least one scoped coordinate, making its negative Boolean clause true. Thus $x$ supplies a satisfying assignment for ${\phi }_P$.

Conversely, a satisfying assignment selects a unique value $x_i$ for every $X_i$. If a constraint failed, the selected scoped tuple would belong to $F_C$, and its entire negative Boolean clause would be false. That contradicts satisfiability. Hence $x$ is a solution. Decoding takes $O({\sum }_i|D_i|)$ by scanning the value indicators. This proves $P$ has a solution if and only if ${\phi }_P$ is satisfiable.

For explicit size accounting, put $q_i=|D_i|$, $r_C=|S_C|$ and $f_C=|F_C|$. There are ${\sum }_i{q}_i$ Boolean variables,Boolean clauses, andliteral occurrences. These formulas count nonempty scopes; a false zero-arity constraint contributes an empty Boolean clause, while a true one contributes none. Formula storage is $O(K+L)$ literal-sized records; a bit-level encoding also stores indicator indices. With maximum constraint domain size $q$, $m$ constraints and maximum arity $r$, this is bounded by $O(n{q}^2+mr{q}^r)$ for nontrivial domains and scopes. In the common binary case it is $O((n+m)q^2)$.

The input representation matters: listing all forbidden tuples costs up to ${\prod }_{i\in S_C}{q}_i$ tests per constraint. This is polynomial for bounded arity and explicitly represented domains, but can be exponential in the description length of a succinct high-arity constraint. The translation is valid in that case without constituting a polynomial-size reduction. If a compact constraint is supplied as a polynomial-size Boolean circuit, one may instead encode that circuit using auxiliary Boolean variables and local conjunctive normal form equivalences, with size proportional to the circuit. No compact representation is silently assumed.

For the instance in (c), after unary filtering there are $17$ indicators. The five at-least-one Boolean clauses, $22$ pairwise at-most-one Boolean clauses and $24$ forbidden-equality Boolean clauses give $51$ Boolean clauses. Setting only $p_{a,1},p_{b,2},p_{c,3},p_{d,2},p_{e,1}$ true encodes the displayed solution.

For one input bit, a Boolean function is specified by the pair $(f(0),f(1))$, and $k=f(0)+f(1)$ counts its satisfying assignments. In the ordered computational basis $(|0⟩,|1⟩)$, the supplied phase oracle convention givesHere $\oplus$ is exclusive or: the oracle changes the sign of the inputs with $f(x)=0$. With $I$ the identity matrix and $Z$ the Pauli Z gate, all four cases areThe two middle cases are balanced Boolean functions; the others are constant functions. The specified zero-state sign change and the Hadamard gate are

Use the top qubit as the first tensor product factor. Write the controlled unitary gate as $C(V)=|0⟩⟨0|\otimes I+|1⟩⟨1|\otimes V$. Reading the bracketed quantum circuit from left to right, its four operations are $C(U_f)$, $C(H)$, $C(U_0)$, $C(H)$. Thus the target operation in its control-one branch iswhere the rightmost matrix acts first. The control-zero branch is the identity operator. The Hadamard conjugation of a controlled gate identity givesIndeed, on control zero the replacement applies $HIH=I$ to the target, while on control one both sides apply $H{U}_{0}H$. By linearity, the identity holds on every quantum superposition and therefore in every repetition of the bracket. This replaces the two internal controlled Hadamard gates as a pair.

The global phase of a controlled quantum gate must be preserved: $C(-I)=Z\otimes I$, whereas $C(I)=I\otimes I$. Consequently the minus signs in $U_0=-Z$ and the special phase oracles $U_f=-I,-Z$ cannot be discarded as an unobservable global phase of the complete quantum circuit.

The succinct input is the players' variable-control sets, their goal propositional formulas, and a complete candidate Boolean valuation; an exponentially expanded payoff matrix is not part of the input. This representation is essential to candidate equilibrium checking in a Boolean game.

For membership in co-NP, consider the complement: the candidate is not a Nash equilibrium. A complexity certificate consists of a player $i$ and an alternative Boolean valuation of that player's controlled Boolean variables. Evaluate the current goal and the goal after this unilateral deviation, keeping every other player's variables fixed. A profitable unilateral deviation exists precisely when the current goal is false and the new goal is true. The certificate has at most the number of input variables plus the player index, and both propositional formula evaluations take polynomial time. Thus the complement belongs to NP, and the original decision problem belongs to co-NP.

For hardness, start with a propositional formula $F(X)$ and introduce a fresh Boolean variable $z$. Construct a one-player Boolean game in which that player controls $X\cup \{z\}$ and has goalChoose the candidate pure strategy assigning every variable false. Its payoff is zero because $z$ is false, regardless of $F$. If $F$ has a satisfying assignment, changing $X$ to that assignment and $z$ to true is a profitable unilateral deviation. If $F$ is an unsatisfiable Boolean formula, no unilateral deviation can satisfy the goal. ThereforeThe construction increases the formula length by only a constant and writes a candidate of linear length, so it is a polynomial-time many-one reduction. Unsatisfiability is co-NP-complete; combining hardness and membership proves that candidate Nash equilibrium checking for Boolean games is co-NP-complete. If a convention requires at least two players, add a player controlling a fresh unused variable and having the always-true goal; this changes neither direction of the proof.

Repeated use of $U\to V\equiv \neg U\vee V$ yieldsThis logical disjunction is false exactly when $A_2,\dots ,A_n$ are all true and $A_1$ is false. There is precisely one such Boolean valuation out of the $2^n$ assignments to the $n$ independent propositional variables. Thus the number of satisfying assignments is $2^n-1$. This is the satisfying-assignment count for nested implications; the implication brackets associate to the right here.

Use $0$ and $1$ for false and true truth values. The truth table is:

The two satisfying rows with $A=B=1$ combine by eliminating $C$, while the remaining satisfying row has $A=B=0,C=1$. An equivalent disjunctive normal form is thereforeExpanding the logical biconditional into its two implications, and using $\neg B\to C\equiv B\vee C$, gives the conjunctive normal formEach form has exactly the same three satisfying assignments as the original propositional formula.

Interpret $x_1,\dots ,x_n$ as the bits of a binary number, with $x_1$ most significant. Construct a propositional formula saying that this number is strictly less than $k$. This gives a quadratic-size formula with prescribed model count.

For $0<k<2^n$, write $k=(b_1\cdots b_n{)}_2$. For each $i$ with $b_i=1$, define the conjunctionThe empty prefix for $i=1$ is omitted. Let ${\phi }_k={\bigvee }_{i:b_i=1}{T}_i$. A Boolean valuation satisfies $T_i$ exactly when its first difference from the binary representation of $k$ is at position $i$, changing a one of $k$ to a zero. All later bits are unrestricted. Hence these cases are disjoint and cover exactly the numbers $0,\dots ,k-1$.

Alternatively, counting the disjoint cases directly givesEach $T_i$ has length $O(i)$, including its logical connectives and parentheses; the total length is at most a constant multiple of ${\sum }_{i=1}^{n}i=O(n^2)$. The endpoints are ${\phi }_0=\perp$ and ${\phi }_{2^n}=\top$. If constants are unavailable and $n\ge 1$, use $x_1\wedge \neg x_1$ and $x_1\vee \neg x_1$ instead. Assignments are counted over all $n$ specified variables, including any absent from the formula. For $n=0$, the constants describe the two possible counts, zero and one. Thus the construction covers $0\le k\le 2^n$, including the endpoint zero despite the source's word “positive”.

For example, $n=4,k=11=(1011{)}_2$ gives the disjoint cases $0\ast \ast \ast$, $100\ast$ and $1010$, with $8+2+1=11$ satisfying assignments.

For each $0\le k\le 2^n$, a propositional formula over $n$ specified variables can have exactly $k$ satisfying assignments and length $O(n^2)$. For $0<k<2^n$, interpret a Boolean valuation as the binary number $x_1\cdots x_n$ and test whether it is less than $k=b_1\cdots b_n$.

For every position $i$ with $b_i=1$, use a conjunction asserting that all earlier bits equal $b_j$ and $x_i=0$, leaving later bits unrestricted. Take the disjunction of these terms. Each satisfying assignment has a unique first differing position, so the terms are disjoint, and their counts sum to ${\sum }_{i:b_i=1}{2}^{n-i}=k$. Their combined length is $O(1+2+\cdots +n)=O(n^2)$. Use logical falsity and logical truth at the two endpoints. The count is over all $n$ variables, including those absent from an individual term or from the whole 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.