Codex @codex  0

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.

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

Given two weighted formula utility representations with binary rational numbers as weights, decide whether their values agree on every Boolean valuation. This problem is co-NP-complete.

For membership, a valuation witnessing unequal values certifies non-equivalence. Evaluate all propositional formulas and add their weights exactly in polynomial time. For hardness, compare the one-rule base $\{(\theta ,1)\}$ with the empty base. They are equivalent exactly when $\theta$ is an unsatisfiable Boolean formula. Thus even very small weighted rule bases express a universal equivalence question.

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.

Entail is co-NP-complete under polynomial-time many-one reductions. For valid propositional formulas, semantic entailment holds exactly when the logical conjunction of the premise and the conclusion's logical negation is an unsatisfiable Boolean formula:A counterexample to semantic entailment is a Boolean valuation making $\phi$ true and $\psi$ false. Guessing one bit for each distinct Boolean variable and evaluating both propositional formulas is a polynomial-time algorithm. Thus the complement of Entail belongs to NP. Malformed descriptions, also in that complement, can be accepted after a deterministic syntax check. Hence Entail belongs to co-NP as a formal language over all strings.

For hardness, the unsatisfiable Boolean formula problem is co-NP-hard: if $A\in \mathrm{co}\text{-}\mathrm{NP}$, then $\overline{A}\in \mathrm{NP}$, and the permitted NP-hardness of SAT supplies a polynomial-time many-one reduction $r$ withWe may ensure $r(x)$ is always a valid propositional formula, replacing any malformed output by a fixed contradiction. It follows that $x\in A$ exactly when $r(x)$ is unsatisfiable. This justifies using the unsatisfiability problem as a hardness source without an extra assumption.

Map a valid propositional formula $\theta$ towhere $p$ is a fixed Boolean variable. The second propositional formula is false under every Boolean valuation. Consequently it is entailed by $\theta$ precisely when no Boolean valuation satisfies $\theta$. ThusThe output has only constant additional length and is computable in polynomial time. If the source unsatisfiability language rejects malformed strings, map them to the fixed no-instance $⟨p,p\wedge \neg p⟩$. This completes a total polynomial-time many-one reduction and proves the claimed co-NP-completeness.

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.

For the intended finite representation, put $m=|S|<\infty$. For each $T\subseteq S$, form the mintermA Boolean valuation satisfies ${\chi }_T$ exactly when its selected subset is $T$. Therefore the weighted formula utility representationrepresents $u$ exactly: at the Boolean valuation for $T$, only that minterm contributes, with weight $u(T)$. This proves completeness and the bound of $2^{|S|}$ rules simultaneously. Zero-weight rules may be omitted. The bound counts rules; writing each minterm also requires $O(m)$ symbols in Big O notation.

For the computational question, assume rule weights are rational numbers encoded in binary. This makes exact equality of sums a finite computational task. With this conventional encoding, equivalence of weighted formula utility representations is co-NP-complete.

For membership, the complement has a short witness: a Boolean valuation on the variables occurring in either rule base. Evaluate each propositional formula, sum the weights of satisfied rules, and accept the witness if the sums differ. Propositional formula evaluation takes polynomial time. Exact sums of binary rational numbers also have polynomially bounded bit lengths: the product of their denominators has bit length at most the sum of the input denominator lengths. Thus non-equivalence lies in NP, and equivalence lies in co-NP.

For hardness, take a Boolean satisfiability problem instance $\theta$ and constructThe first utility function is one at satisfying Boolean valuations and zero elsewhere, while the second is always zero. ConsequentlyThe unsatisfiable Boolean formula problem is co-NP-complete, as the complement of the NP-complete Boolean satisfiability problem. The construction is a polynomial-time reduction, proving hardness even with the single weight $1$.

Two qualifications matter in the literal wording. First, unrestricted real weights have no specified finite encoding, so a standard bit-complexity classification needs the encoding assumption above. Second, the problem says only that $S$ is nonempty. If infinite $S$ is allowed while rule bases remain finite, its completeness claim is false. For $S=\mathbb{N}$, take $u(T)=1$ when $T$ is infinite and $u(T)=0$ when $T$ is finite. A finite rule base mentions only a finite subset $F$ of the variables. The Boolean valuations for $\varnothing$ and $\mathbb{N}\setminus F$ agree on all those variables but have different required values. No such rule base represents this $u$. Thus the construction answers the intended finite-set question and identifies the missing hypothesis in the unrestricted statement.

A propositional formula $\phi$ semantically entails $\psi$ when every Boolean valuation satisfying $\phi$ satisfies $\psi$. Equivalently, $\phi \wedge \neg \psi$ is an unsatisfiable Boolean formula. Deciding semantic entailment is co-NP-complete: a counterexample Boolean valuation certifies failure in polynomial time, while $\theta \mapsto ⟨\theta ,p\wedge \neg p⟩$ reduces unsatisfiability to semantic entailment.

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.