Codex @codex  0

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.

A finite game represented succinctly by propositional logic. Each player controls a disjoint collection of Boolean variables and chooses their truth values. Together those choices determine a Boolean valuation. A player's goal is a propositional formula, with payoff one if satisfied and zero otherwise. The control sets normally form a set partition of all variables.

A pure strategy strategy profile is a Nash equilibrium if every unsatisfied player remains unsatisfied after every change to that player's controlled variables. Checking a candidate can therefore require solving a Boolean satisfiability problem, even though evaluating its current payoffs is easy.

A Boolean literal is a Boolean variable $u$ or its logical negation $\neg u$. The two Boolean literals have opposite truth values: a Boolean valuation $v$ gives $v(\neg u)=1-v(u)$ when false and true are encoded as zero and one. Thus $u=0$ makes the positive Boolean literal $u$ false and the negative Boolean literal $\neg u$ true. A Boolean clause combines Boolean literals, and a Boolean-pair colouring gadget represents a Boolean variable and its logical negation by two vertices with opposite Boolean colours.

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.

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.

A cardinality constraint restricts how many members of a specified collection are selected or satisfy a property. For Boolean variables, exactly $k$ selected entries gives the displayed sum; upper and lower bounds give at-most and at-least variants. Constraint propagation can maintain the number already selected and the number still available. A requirement involving many variables is a global constraint, even when it has a compact arithmetic description.

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.

A restriction requiring exactly one member of a set of Boolean variables to be true. A direct conjunctive normal form encoding combines one at-least-one Boolean clause, $p_1\vee \cdots \vee p_q$, with $\left(\genfrac{}{}{0ex}{}{q}{2}\right)$ at-most-one Boolean clauses, $\neg p_i\vee \neg p_j$ for $i<j$. The first supplies existence and the second supplies uniqueness. For $q=0$, the empty at-least-one Boolean clause correctly makes the condition unsatisfiable.

Every finite collection of finite propositional formulas mentions only finitely many Boolean variables. Two Boolean valuations agreeing on those variables satisfy exactly the same formulas. They therefore have the same value under any weighted formula utility representation using that collection.

This observation limits representation over infinite sets. On $\mathbb{N}$, the function indicating whether the selected subset is infinite cannot be represented by a finite rule base: if $F$ is the finite set of mentioned indices, $\varnothing$ and $\mathbb{N}\setminus F$ agree on all those indices but require values zero and one. Completeness claims for finite propositional rule bases must therefore specify a finite underlying set or restrict the functions represented.

A truth table arranged so neighbouring cells differ in one Boolean variable, using Gray code order along each multi-bit axis. Opposite edges are also adjacent. A valid group contains all $2^k$ combinations of $k$ varying variables while every other variable stays fixed; it eliminates those $k$ variables and gives an implicant; covering the one-cells yields a disjunctive normal form. The method is associated with Maurice Karnaugh.

A conjunction containing each of a specified finite collection of Boolean variables exactly once, either positively or negated. It is satisfied by exactly one Boolean valuation of those variables. The minterms for all valuations are mutually exclusive and collectively exhaustive, so they can encode an arbitrary finite table of values.

Choose $k$ distinct squares of an $n\times n$ chessboard so that no chosen pair has absolute coordinate differences $(1,2)$ or $(2,1)$. One constraint satisfaction problem representation has $k$ square-valued variables, requiring distinctness and pairwise nonattack. Another has one Boolean variable per square, a cardinality constraint fixing their sum to $k$, and one mutual-exclusion constraint for every edge of the knight attack graph. The first has fewer variables when $k$ is small but represents each unlabelled placement up to $k!$ times; the second uses only binary constraint domains and sparse local attack restrictions.

On a finite rectangular Conway's Game of Life board stored as an array of Boolean variables, retain the preceding row's old values in one auxiliary row. Before overwriting a column, retain rolling sums of the old three-cell vertical columns. Their sum minus the old center is the old neighbor count. Read the next column before changing the current one; replace the saved row entry by the old current cell. The invariant is that every count uses the previous generation, just as in the two-array algorithm. For a board with $H$ rows and $W$ columns this uses $O(W)$ auxiliary storage and $O(HW)$ time. The boundary convention must still be implemented explicitly. The Life blinker and Life glider provide exact expected generations for checking it.

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.

Let $Q=\{1,\dots ,n{\}}^2$ be the board squares and let $\mathrm{Attack}(p,q)$ mean that the absolute coordinate differences are $(1,2)$ or $(2,1)$.

One variable per knight. Use $X_1,\dots ,X_k$, with each constraint domain equal to $Q$. For every pair $i<j$, requireEvery satisfying assignment places $k$ distinct nonattacking knights, and any such placement gives an assignment after labelling its knights. This has only $k$ variables and $O(k^2)$ binary constraints, but domains of size $n^2$. Relabelling the knights gives $k!$ assignments for the same unlabelled board, so the representation contains considerable redundancy.

One Boolean variable per square. Use $Y_q\in \{0,1\}$ for every $q\in Q$. Impose the cardinality constraintand for every knight-attack pair $p,q$ impose $Y_p+Y_q\le 1$. There are $n^2$ variables, each with a two-element constraint domain, and only $O(n^2)$ local attack restrictions, because each square attacks at most eight others. The single counting constraint is a global constraint, not a binary constraint.

The square encoding avoids knight-label redundancy and has sparse local attack relations; the knight encoding uses fewer variables when $k$ is small and makes single-knight moves natural. Both are exact representations of the nonattacking knights problem. Neither may impose one knight per row: several knights can legally share a row.

Use a sequential SATPlan encoding with times $t=0,\dots ,T$. The fluent universe isThere are nine support Boolean variables and three clearance Boolean variables per time layer. Static block types, parameter inequalities and permanent table availability are handled during action grounding. For each well-typed ground action $a$ from parts (b)–(c), introduce an occurrence Boolean variable $a_t$ for $0\le t<T$. Allow at most one action per layer, including no action, so that a horizon of $T$ encodes at most $T$ physical actions.

The complete initial-state formula isEvery well-typed fluent not initially true is explicitly false. The final goal formula is simply $G_T=\mathrm{On}(A,B{)}_T\wedge \mathrm{On}(B,C{)}_T$. Leaving unrelated final facts unconstrained is appropriate; leaving unrelated initial facts unconstrained would introduce imaginary starting states.

For each $t<T$, include all action precondition axioms $a_t\to {\bigwedge }_{p\in \mathrm{Pre}(a)}{p}_t$, after removing static true conditions. For example,The precondition axiom for $\mathrm{MoveToTable}(C,A{)}_t$ similarly requires $\mathrm{On}(C,A{)}_t\wedge \mathrm{Clear}(C{)}_t$.

For every fluent $p\in \mathcal{P}$, let ${\mathrm{Add}}_p(t)$ be the logical disjunction of actions at $t$ adding $p$, and ${\mathrm{Del}}_p(t)$ the logical disjunction deleting it. Include the successor-state axiomIt combines action effects with the frame axiom, preventing unsupported changes. A fully grounded example isApply the same construction to every support and clearance fluent, using the exact add/delete lists. If no action occurs, both effect logical disjunctions are false, so all fluents persist.

The sequential action exclusion axioms are $\neg a_t\vee \neg b_t$ for every pair of distinct grounded actions $a,b$. For example,forbids selecting those two occurrences together. Do not add a requirement that some action occur in every layer: that would remove idle padding and change “at most $T$” into an exact-length requirement. One may additionally include true planning state invariants, such as a block having at most one support and a block support carrying at most one block; the unlimited table must be exempt from the latter restriction.

Finally, conjoin $I_0$, $G_T$, and all precondition, successor and exclusion formulas over the layers to obtain ${\phi }_T$. It is a propositional formula; if a solver requires conjunctive normal form, use a satisfiability-preserving Tseitin transformation with auxiliary Boolean variables. The equivalence between this encoding and real action sequences follows from sequential SATPlan correctness: a satisfying assignment induces exactly the stated STRIPS trajectory, and every sufficiently short valid plan supplies such an assignment.

Read the satisfying assignment in increasing time order. In layer $t$, output the unique ground action whose occurrence Boolean variable is true, or output nothing if all are false. Discard idle layers. The result is a sequence of at most $T$ actions.

For correctness, the layer-zero planning fluents are exactly the actual initial state. The action precondition axioms make the selected action applicable, while the successor-state axioms give precisely its add/delete update; the action exclusion axioms prevent simultaneous competing actions. By induction, every following time layer is the real state reached by the decoded prefix. The final goal formula therefore proves that the extracted plan reaches both required goals.

Conversely, execute any valid plan of length at most $T$, assign each layer its actual fluent values and pad with idle layers. These values satisfy every component of ${\phi }_T$. In this instance, decoding the three-action trajectory in part (d) gives a model at $T=3$ and at every larger horizon after padding; direct state-space and propositional checks find no model for $T<3$.

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.

Minimax search applies because this is a finite, deterministic two-player zero-sum game with perfect information. Each move assigns a previously unassigned Boolean variable, so play terminates after exactly $N$ moves. Both players observe the whole partial Boolean valuation, and there are no chance moves. Give terminal positions payoff $+1$ when the propositional formula is true and $-1$ when it is false, measured for $A$. At an $A$-node take the maximum child value and at a $B$-node the minimum. Backward induction then computes the winner and a corresponding winning strategy.