Polynomial-time reduction

A polynomial-time reduction transforms instances of one computational problem into instances of another using a polynomial-time algorithm.

A polynomial-time many-one reduction from a decision problem $A$ to a decision problem $B$ is a polynomial-time computable function $r$ satisfying $x\in A$ exactly when $r(x)\in B$.

A total mapping $f$ with $x\in A$ exactly when $f(x)\in B$, computed by a deterministic logarithmic-work-space transducer with read-only input and write-only output. Such reductions compose, and are used for NL-completeness and P-completeness. The output can be polynomially larger than the work storage.

A decision problem is NP-hard when every problem in NP polynomial-time many-one reduces to it.

A decision problem is NP-complete when it is both in NP and NP-hard.

Given subsets $S_1,\dots ,S_m$ of a finite universe, the decision problem asks whether at most $k$ of them cover the universe. It is NP-complete. If $k<m$, existence of a cover by at most $k$ subsets is equivalent to existence of a cover by exactly $k$, by adding unused subsets. The promise that every element occurs in some subset loses no hardness: an uncovered element can be detected in polynomial time and mapped to a fixed negative instance.

// Target: mathematical-optimization.bigb

Assume $2\le k<m$ and ${\bigcup }_i{S}_i=S$. Construct a two-player game with row $i$ for $S_i$ and columns $0,1,\dots ,n$. Column $0$ pays both players one; column $j>0$ pays $(1,0)$ when $j\in S_i$, and $(0,k/(k-1))$ otherwise. There is a Nash equilibrium whose row player's support of a mixed strategy has size $k$ exactly when $k$ rows cover the universe. A uniform mixture on a cover makes column $0$ a best response. Conversely, if some element is uncovered by the support, the column player's best responses are uncovered elements and the row player's current payoff is zero. The union promise provides a profitable row deviation. Without the union promise the equivalence is false: a globally uncovered element is a best response against every row mixture.

// Target: mathematical-optimization.bigb

Every NP verifier can be compiled into a polynomial-size Boolean circuit whose inputs encode its certificate, and then into an equisatisfiable conjunctive normal form by a Tseitin transformation. This gives a polynomial-time many-one reduction from every NP language to SAT. Checking a guessed assignment proves membership, so SAT is NP-complete.

Given finitely encoded nonnegative integers $s_i$ and target $t$, the subset sum problem asks whether some subset sums to $t$. Taking equal item weights and profits reduces it to testing whether a 0-1 knapsack problem with capacity $t$ attains value $t$.

For indexed occurrences with positive integer weights, let $D_i(t)$ record whether a subset of the first $i$ entries has sum $t$. The recurrence chooses whether the last occurrence is absent or present: $D_i(t)=D_{i-1}(t)\vee D_{i-1}(t-a_i)$, with an out-of-range term false. Initialize only sum zero true. Descending one-dimensional updates prevent reusing the current occurrence. Time is $O(ns)$ for target $s$ and space $O(s)$; positivity permits immediate rejection above the total. With weights bounded by $k$, the total is at most $nk$, making the bound polynomial in $n,k$.

A finite set $A$ of positive integers such that nonempty disjoint sets contained in $A$ have different sums, and the larger subset has the larger sum when their sizes differ. For $a_1<\cdots <a_n$, the size condition is equivalent to $a_1+\cdots +a_{k+1}>a_{n-k+1}+\cdots +a_n$ for $1\le k\le \lfloor (n-1)/2\rfloor$: the left side is the smallest possible sum of $k+1$ elements and the right side the largest sum of $k$ elements.

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.

An algorithm or software system that decides whether a Boolean formula has a satisfying assignment, usually returning one when it exists. Unit propagation and clause learning are important mechanisms in modern SAT solvers. A reduction must be correct and its representation costs counted before the performance of the downstream SAT solver is relevant.

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.

If all but one literal of a Boolean clause are false under a partial Boolean valuation, the remaining literal must be true in any extension satisfying the clause. Repeatedly make such forced assignments, remove satisfied Boolean clauses and remove false literals from the others. An empty Boolean clause proves that the current partial Boolean valuation has no satisfying extension. This is sound because every step is forced by an original or already implied Boolean clause; it is not by itself a complete SAT decision procedure.

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.

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.

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.

For a CNF input with $n$ Boolean variables, $m$ Boolean clauses, and $L$ Boolean literal occurrences, first check that the supplied Boolean valuation gives each input Boolean variable exactly one truth value. Evaluate each Boolean literal by lookup or logical negation, each Boolean clause by logical disjunction, and the Boolean formula by logical conjunction. Indexed Boolean variables and constant-cost lookups give an $O(n+m+L)$ operation count; with a finite binary string encoding the check still takes polynomial time. Thus a satisfying assignment is a certificate in computational complexity for SAT, proving that SAT belongs to NP. Finding it by exhaustive checking can require $2^n$ candidate Boolean valuations; this enumeration cost is not a lower bound on every possible SAT algorithm.^[ref]

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.

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.

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.

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.

Maximum satisfiability asks for a truth assignment maximizing the number of true clauses of a conjunctive normal form formula. The Boolean satisfiability problem asks whether all its clauses can be made true. Binary clause indicators give an integer programming formulation, and the literal-frequency greedy approximation for MAX-SAT guarantees at least half the optimum. Counts of clauses, rather than multiplicities of repeated literals within one clause, are relevant to this objective.

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.

Satisfiability of conjunctive normal form formulas whose clauses have at most two unnegated variables. It is NP-complete: binary AND/OR and unary NOT gate equivalences in a Tseitin transformation already satisfy that restriction. Clauses may contain arbitrarily many negative literals; the total clause width is not restricted to two.

Maximum 2-satisfiability asks for an assignment satisfying as many clause occurrences as possible when every nonempty clause has at most two literals. Occurrences are counted even when a clause is repeated. Its decision problem is NP-complete by the seven-clause gadget for MAX-2SAT, while the method of conditional probabilities gives a polynomial-time half approximation.

When each variable appears in at most one normalized singleton clause, satisfy that favored literal with probability $p>1/2$ and choose independent variables. Every proper binary clause is then satisfied with probability at least $1-p^2$, and every singleton with probability $p$. Maximize the common lower bound by $p=1-p^2$, giving the reciprocal of the golden ratio. The method of conditional probabilities derandomizes the construction, obtaining approximation ratio $p$. Tautologies are harmless; the singleton restriction must be applied after removing repeated literals within clauses.

A three-literal disjunction can be represented by ten unit or two-literal clause occurrences with one fresh auxiliary variable. If the number $r$ of true input literals is zero, the best auxiliary choice satisfies six; for $r=1,2,3$, the best count is seven. Applying separate gadgets to all clauses of a 3-SAT instance gives target seven times the original clause count, proving NP-completeness of the decision form of MAX-2SAT. The local counting argument is essential: no gadget may exceed seven and compensate for an unsatisfied input clause.

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

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.

Introduce a Boolean variable for each gate output and impose its equivalence to the gate's input function with a constant number of clauses. A final unit clause forces acceptance. For a bounded-fan-in Boolean circuit, the formula size is linear in the gate count and it is satisfiable exactly when some input makes the Boolean circuit output one. Auxiliary variables extend the satisfying assignments; this is equisatisfiability, not equality as functions of the enlarged variable set.

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.

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.

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.

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 Horn clause is a disjunction of literals containing at most one positive literal. It can be read as an implication whose antecedent is a conjunction of variables.

Horn-SAT asks whether a conjunction of Horn clauses is satisfiable.

The Horn-SAT forward-chaining algorithm starts with every variable false and repeatedly makes the conclusion of any enabled implication true. It reports failure if it enables a clause with no positive conclusion; otherwise the fixed point is the least satisfying assignment.

Quadratic-equation satisfiability over ${\mathbb{F}}_2$ asks whether a finite system of polynomial equations of degree at most two over the finite field ${\mathbb{F}}_2$ has a common solution.

If $\mathbf{P}\ne \mathbf{NP}$, then NP contains a decision problem that is neither in P nor NP-complete.