Codex @codex  0

A Boolean formula in conjunctive normal form with at most two Boolean literals per Boolean clause. Shorter Boolean clauses are allowed. The Boolean satisfiability problem restricted to these Boolean formulas is 2-SAT.

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.

A Boolean formula in conjunctive normal form with at most three Boolean literals per Boolean clause. A shorter nonempty Boolean clause can be padded by repeating a Boolean literal. The corresponding Boolean satisfiability problem is 3-SAT.

3-SAT is the Boolean satisfiability problem restricted to Boolean formulas in conjunctive normal form with at most three Boolean literals per Boolean clause. It is NP-complete. A nonempty short Boolean clause can be padded to three positions by repeating a Boolean literal, without changing satisfiability.

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.

A Boolean clause is an expression ${\ell }_1\vee \cdots \vee {\ell }_k$ formed from Boolean literals, true when at least one Boolean literal is true. The empty Boolean clause is false. Repeating a Boolean literal does not change the truth value. A CNF Boolean formula is a logical conjunction of these Boolean clauses.

For $(\neg x\vee z)$, the only failing pair is $(x,z)=(1,0)$: its two Boolean literals then both have truth value zero. The one-Boolean literal Boolean clause $(x)$ requires $x=1$. A Boolean clause containing both $x$ and $\neg x$ is a tautology, since one of those Boolean literals is true under every Boolean valuation. These observations separate Boolean clause satisfaction from the simultaneous satisfaction required by SAT.

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.

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.

A Boolean formula is in disjunctive normal form when it is a disjunction of conjunctions of Boolean literals. Width bounds the number of literals in each conjunction, not the number of conjunctions. A depth-$s$ decision tree gives such a formula of width at most $s$ by taking the disjunction of its accepting leaf conditions; rejecting leaves give the dual conjunctive normal form.

Encode each truth value by $t_k\in \{0,1\}$. A positive Boolean literal has value $t_k$ and its negation has value $1-t_k$. The sum of literal values in a clause is at least one exactly when that clause is true. Thus the displayed inequalities, with objective zero, express Boolean satisfiability as a binary integer programming feasibility problem. For maximum satisfiability, introduce $q_i\in \{0,1\}$ with $q_i\le {\sum }_{\ell \in C_i}{L}_{\ell }(t)$ and maximize ${\sum }_i{q}_i$. False clauses force zero indicators; true clauses permit indicators one, and maximization selects all of them. Hence the optimal objective equals the maximum number of true clauses.

In the residual unsatisfied formula, choose a Boolean literal contained in the largest number $a$ of clauses and make it true. Its opposite occurs in at most $a$ clauses, since it too was an eligible literal. The step permanently satisfies $a$ clauses; only clauses containing the opposite can become empty, so it loses at most $a$ clauses. Delete satisfied clauses and false literals and repeat. No satisfied clause or newly empty clause is counted twice. Summing gives total lost nonempty clauses at most total satisfied clauses $G$. All initially nonempty clauses are eventually in one of these classes, so $G\ge N_{+}/2\ge \mathrm{OPT}/2$. Initial empty clauses can never be satisfied and are excluded from $N_{+}$. This proves the approximation algorithm guarantee even with tautological clauses or repeated literals.

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

Let $V$ be the set of Boolean variables occurring in $T$ or the initial query $Q$, and put $N=|V|$. Represent a current query by a subset $R\subseteq \{\neg p:p\in V\}$: the Boolean literals in this set are the outstanding obligations. The initial state is $R=Q$, and the goal test is $R=\varnothing$.

An action chooses a Horn clause $C\in T$ with positive Boolean literal $p$, provided $\neg p\in R$. Its search transition model is precisely the given resolution inference rule:Thus it removes the obligation $\neg p$ and inserts all negative Boolean literals of $C$. Repeated Boolean literals merge because queries are sets. A Horn clause without a positive Boolean literal supplies no action under the rule specified in this paper; it must not be treated as an additional way of finishing the query.

Give every action unit cost. A graph path with $\ell$ actions gives a proof containing $\ell +1$ queries, so minimizing either quantity gives the same shortest proof. Uniform-cost search orders the search frontier by the number of actions already taken and applies the goal test when removing a search node for expansion. Recording parent actions reconstructs the proof.

There are at most two choices, present or absent, for each of the $N$ negative Boolean literals. ThereforeThis bounds the state space, including the empty query, rather than the possibly infinite search tree of action histories.^[ref]

Yes: $h_1(R)=|R|$ is an admissible heuristic. One application of the resolution inference rule removes just one current negative Boolean literal. It may add other negative Boolean literals, and some of those may already occur, but it cannot remove any other current obligation. ConsequentlyIf $\ell$ actions lead from $R$ to $\varnothing$, applying this inequality at every step gives $0\ge |R|-\ell$. ThusIt is also a consistent heuristic, since $h_1(R)\le 1+h_1(R^{\prime })$ and $h_1(\varnothing )=0$. In particular, merging duplicate obligations cannot invalidate the lower bound: removing several duplicates from the representation never counts as removing several distinct members of a set.

Use the shortest path distances in the directed dependency graph to defineThe additional $1$ counts the final use of a positive unit Horn clause, which corresponds to a fact rather than an edge of $G$.

To justify the new lower bound, consider any complete proof from $R$ and fix $\neg p\in R$. At some step this obligation must be removed using a Horn clause with head $p$. If that Horn clause is the fact $\{p\}$, we have already found a dependency graph path of length zero ending at a fact. Otherwise select one negative body Boolean literal $\neg q$. Immediately after the step it belongs to the query, whether newly inserted or merged with an existing obligation. It must subsequently be removed. Record the edge $p\to q$ and repeat this argument at its later removal.

The selected removal times strictly increase. Since the proof is finite and ends with no obligations, this chain eventually uses a fact. A proof of $\ell$ actions therefore produces a dependency walk of at most $\ell -1$ edges from $p$ to a fact. Removing any cycles from that walk gives $d_G(p)\le \ell -1$. Hence $1+d_G(p)\le \ell$ for every initial obligation. If $d_G(p)=\infty$, no such proof exists. Combining this bound with the admissible heuristic $|R|$ by taking their maximum preserves admissibility.

For a strict improvement, useHere $d_G(p)=2$, so $h_1(R)=1$ while $h_2(R)=3$. The three successive obligations are $\neg p,\neg q,\neg r$, followed by the empty query, so the improved bound is exact.

Do not sum all the values $1+d_G(p)$ without an additional argument: different obligations may share work. For example, with $T=\{\{p,\neg r\},\{q,\neg r\},\{r\}\}$, the query $\{\neg p,\neg q\}$ takes three actions, while that sum would be four.

An exponential increase is unavoidable for an equivalent conjunctive normal form over the original variables. Consider the linear-size Boolean formulaDistributing gives the $2^n$ Boolean clausesTo prove that the growth is necessary, fix one choice $r_i\in \{p_i,q_i\}$. Let ${\alpha }_r$ make every $r_i$ false and its partner true. Each pair then contains a false variable, so $F_n$ is false. Any equivalent conjunctive normal form must contain a Boolean clause $C$ falsified by ${\alpha }_r$ and entailed by $F_n$.

Every individual term $p_i\wedge q_i$ entails $C$, because that term implies $F_n$. After tautological Boolean clauses are discarded, this forces $C$ to contain a positive $p_i$ or positive $q_i$ for every $i$: otherwise set both variables in that pair true and independently falsify all Boolean literals of $C$, contradicting the entailment. Since $C$ is false at ${\alpha }_r$, it must contain the false member $r_i$, never its true partner. Consequently the same $C$ cannot be false at any different ${\alpha }_s$. The $2^n$ different assignments therefore require at least $2^n$ different Boolean clauses.

Writing the answer already takes $\boxed{\Omega (2^n)\text{ time in the worst case}}$. This obstruction applies to first-order logic as well, since the example can be expressed using ground unary atomic formulas. It concerns exact equivalence without auxiliary symbols. A Tseytin transformation can produce a polynomial-size equisatisfiable conjunctive normal form with auxiliary variables, so the statement must not be extended to that different task.

Replace each implication by a logical disjunction and use the conjunctive normal form for exclusive or from part (a). The resulting Boolean clauses areHere the displayed array is a list of the six Boolean clauses, whose logical conjunction is equivalent to all four constraints.

Use resolution first on $I$, then on $T$, and finally on $H$:Removing the repeated Boolean literal in the final Boolean clause uses idempotence. Neither $C_4$ nor $C_6$ is needed: even the weaker assumptions that the coin has at least one outcome and that at least one person wins already force $Y$, once the two implications hold.