Community hub
0 subscribers7 pages, 0 posts
Recent from talks
All channels
Be the first to start a discussion here.
Be the first to start a discussion here.
Be the first to start a discussion here.
Be the first to start a discussion here.
Contribute something
Welcome to the community hub built to collect knowledge and have discussions related to Circuit satisfiability problem.
Nothing was collected or created yet.
Circuit satisfiability problem
View on Wikipediafrom Wikipedia
In theoretical computer science, the circuit satisfiability problem (also known as CIRCUIT-SAT, CircuitSAT, CSAT, etc.) is the decision problem of determining whether a given Boolean circuit has an assignment of its inputs that makes the output true.[1] In other words, it asks whether the inputs to a given Boolean circuit can be consistently set to 1 or 0 such that the circuit outputs 1. If that is the case, the circuit is called satisfiable. Otherwise, the circuit is called unsatisfiable. In the figure to the right, the left circuit can be satisfied by setting both inputs to be 1, but the right circuit is unsatisfiable.
CircuitSAT is closely related to Boolean satisfiability problem (SAT), and likewise, has been proven to be NP-complete.[2] It is a prototypical NP-complete problem; the Cook–Levin theorem is sometimes proved on CircuitSAT instead of on the SAT, and then CircuitSAT can be reduced to the other satisfiability problems to prove their NP-completeness.[1][3] The satisfiability of a circuit containing arbitrary binary gates can be decided in time .[4]
Proof of NP-completeness
[edit]Given a circuit and a satisfying set of inputs, one can compute the output of each gate in constant time. Hence, the output of the circuit is verifiable in polynomial time. Thus Circuit SAT belongs to complexity class NP. To show NP-hardness, it is possible to construct a reduction from 3SAT to Circuit SAT.
Suppose the original 3SAT formula has variables , and operators (AND, OR, NOT) . Design a circuit such that it has an input corresponding to every variable and a gate corresponding to every operator. Connect the gates according to the 3SAT formula. For instance, if the 3SAT formula is the circuit will have 3 inputs, one AND, one OR, and one NOT gate. The input corresponding to will be inverted before sending to an AND gate with and the output of the AND gate will be sent to an OR gate with
Notice that the 3SAT formula is equivalent to the circuit designed above, hence their output is same for same input. Hence, If the 3SAT formula has a satisfying assignment, then the corresponding circuit will output 1, and vice versa. So, this is a valid reduction, and Circuit SAT is NP-hard.
This completes the proof that circuit SAT is NP-Complete.
Restricted variants and related problems
[edit]Planar circuit SAT
[edit]Assume that we are given a planar Boolean circuit (i.e. a Boolean circuit whose underlying graph is planar) containing only NAND gates with exactly two inputs. Planar Circuit SAT is the decision problem of determining whether this circuit has an assignment of its inputs that makes the output true. This problem is NP-complete. Moreover, if the restrictions are changed so that any gate in the circuit is a NOR gate, the resulting problem remains NP-complete.[5]
Circuit UNSAT
[edit]Circuit UNSAT is the decision problem of determining whether a given Boolean circuit outputs false for all possible assignments of its inputs. This is the complement of the Circuit SAT problem, and is therefore co-NP-complete.
Reduction from CircuitSAT
[edit]Reduction from CircuitSAT or its variants can be used to show NP-hardness of certain problems, and provides us with an alternative to dual-rail and binary logic reductions. The gadgets that such a reduction needs to construct are:
- A wire gadget. This gadget simulates the wires in the circuit.
- A split gadget. This gadget guarantees that all the output wires have the same value as the input wire.
- Gadgets simulating the gates of the circuit.
- A true terminator gadget. This gadget is used to force the output of the entire circuit to be true.
- A turn gadget. This gadget allows us to redirect wires in the right direction as needed.
- A crossover gadget. This gadget allows us to have two wires cross each other without interacting.
Minesweeper inference problem
[edit]This problem asks whether it is possible to locate all the bombs given a Minesweeper board. It has been proven to be co-NP-complete via a reduction from circuit UNSAT problem.[6] The gadgets constructed for this reduction are: wire, split, AND and NOT gates and terminator.[7] There are three crucial observations regarding these gadgets. First, the split gadget can also be used as the NOT gadget and the turn gadget. Second, constructing AND and NOT gadgets is sufficient, because together they can simulate the universal NAND gate. Finally, since three NANDs can be composed intersection-free to implement an XOR, and since XOR is enough to build a crossover,[8] this gives us the needed crossover gadget.
The Tseytin transformation
[edit]The Tseytin transformation is a straightforward reduction from Circuit-SAT to SAT. The transformation is easy to describe if the circuit is wholly constructed out of 2-input NAND gates (a functionally-complete set of Boolean operators): assign every net in the circuit a variable, then for each NAND gate, construct the conjunctive normal form clauses (v1 ∨ v3) ∧ (v2 ∨ v3) ∧ (¬v1 ∨ ¬v2 ∨ ¬v3), where v1 and v2 are the inputs to the NAND gate and v3 is the output. These clauses completely describe the relationship between the three variables. Conjoining the clauses from all the gates with an additional clause constraining the circuit's output variable to be true completes the reduction; an assignment of the variables satisfying all of the constraints exists if and only if the original circuit is satisfiable, and any solution is a solution to the original problem of finding inputs that make the circuit output 1.[1][9] The converse—that SAT is reducible to circuit-SAT—follows trivially by rewriting the Boolean formula as a circuit and solving it.
See also
[edit]- Circuit value problem
- Structured circuit satisfiability
- Satisfiability problem
References
[edit]- ^ a b c David Mix Barrington and Alexis Maciel (July 5, 2000). "Lecture 7: NP-Complete Problems" (PDF).
- ^ Luca Trevisan (November 29, 2001). "Notes for Lecture 23: NP-completeness of Circuit-SAT" (PDF). Archived from the original (PDF) on December 26, 2011. Retrieved February 4, 2012.
- ^ See also, for example, the informal proof given in Scott Aaronson's lecture notes from his course Quantum Computing Since Democritus.
- ^ Sergey Nurk (December 1, 2009). "An O(2^{0.4058m}) upper bound for Circuit SAT".
- ^ "Algorithmic Lower Bounds: Fun With Hardness Proofs at MIT" (PDF).
- ^ Scott, Allan; Stege, Ulrike; van Rooij, Iris (2011-12-01). "Minesweeper May Not Be NP-Complete but Is Hard Nonetheless". The Mathematical Intelligencer. 33 (4): 5–17. doi:10.1007/s00283-011-9256-x. ISSN 1866-7414. S2CID 122506352.
- ^ Kaye, Richard (Mar 2000). "Minesweeper is NP-complete" (PDF). The Mathematical Intelligencer. 22 (2): 9–15. doi:10.1007/BF03025367. S2CID 122435790.
- ^ see File:Crossover xor.gif and File:Crossover nand.pdf
- ^ Marques-Silva, João P. and Luís Guerra e Silva (1999). "Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning" (PDF). Archived from the original (PDF) on 2022-07-02.
Circuit satisfiability problem
View on Grokipediafrom Grokipedia
Definition and Fundamentals
Boolean Circuits
A Boolean circuit is formally defined as a directed acyclic graph (DAG) where nodes represent either input variables, constant values (if permitted), output nodes, or logic gates that compute Boolean functions.[3] The edges in the graph indicate directed connections from outputs of predecessor nodes to inputs of successor nodes, ensuring no cycles exist to prevent infinite loops during evaluation.[4] Input nodes correspond to Boolean variables or constants (0 or 1), while output nodes designate the circuit's results, typically one or more Boolean values.[5] The gates in a Boolean circuit are restricted to a finite basis of standard Boolean operations, primarily binary gates such as AND (conjunction, outputting 1 only if both inputs are 1) and OR (disjunction, outputting 1 if at least one input is 1), each with fan-in 2, and unary gates such as NOT (negation, inverting the input from 0 to 1 or vice versa), with fan-in 1.[6] Fan-out refers to the number of edges leaving a node, which is unbounded, allowing a single gate's output to feed into multiple subsequent gates.[7] This structure enables the circuit to model any Boolean function computable by a finite sequence of these operations, with the graph's acyclicity guaranteeing a topological order for evaluation.[8] Two key complexity measures for Boolean circuits are size and depth. The size of a circuit is the total number of gates (excluding input and output nodes).[4] The depth is the length of the longest directed path from any input node to an output node, measured in the number of edges, which reflects the circuit's parallel computation potential.[6] A representative example is a circuit computing the XOR function on two inputs and , which outputs 1 if exactly one input is 1. This can be constructed using five gates: two NOT gates to negate each input, two AND gates to compute and , and one OR gate to combine these results. In textual diagram description, the graph has input nodes for and ; edges from to a NOT gate (producing ) and to an AND gate A1; edges from to a NOT gate (producing ) and to an AND gate A2; edges from to A2 and from to A1; then edges from A1 and A2 to the final OR gate, whose output is the result. Standard notation denotes inputs as Boolean variables , with constants 0 or 1 optionally included as fixed input nodes.[5] Evaluation proceeds by assigning values to inputs and propagating them forward: for a gate with incoming edges from nodes , the value is for AND, for OR, or for NOT, where and are Boolean conjunction and disjunction.[7] Boolean circuits serve as the foundational model for the circuit satisfiability problem, where the task involves finding input assignments that yield specific outputs.[4]Formal Problem Statement
The circuit satisfiability problem, denoted as CIRCUIT-SAT or CSAT, is a decision problem in computational complexity theory. Given a Boolean circuit with input variables and a single output gate, the question is whether there exists an assignment of Boolean values (0 or 1) to the input variables such that the output of evaluates to 1. Formally, the circuit computes a function , and is satisfiable if there exists some such that . The input to CIRCUIT-SAT consists of a description of the Boolean circuit , typically encoded as a list of gates, their types (such as AND, OR, or NOT), and the connections (wires) between them, along with the designations of the input nodes and the single output node. This representation forms a directed acyclic graph (DAG) where input nodes have no incoming edges, and each gate node computes a Boolean operation on its incoming wires. No circuit minimization or optimization is required in the input; the problem accepts any valid circuit description, with the size of the input polynomial in the number of gates and wires. CIRCUIT-SAT is fundamentally a yes/no decision problem, outputting "yes" if the circuit is satisfiable and "no" otherwise. A related search variant, often called the satisfying assignment problem, asks for an explicit input assignment that makes if one exists, but this is not part of the core decision problem. Edge cases include constant circuits, which have no input variables () and always output a fixed value (satisfiable if the constant is 1, unsatisfiable if 0); empty circuits with no gates or paths from inputs to output, which may be considered unsatisfiable by convention unless specified otherwise; and circuits with unreachable output gates, where satisfiability depends on whether any path from inputs can propagate to produce 1 at the output.Computational Complexity
Membership in NP
The class NP consists of all decision problems for which a "yes" instance has a short certificate that can be verified by a deterministic Turing machine in polynomial time.[9] Equivalently, NP contains languages accepted by a nondeterministic Turing machine in polynomial time.[9] The circuit satisfiability problem (CircuitSAT) is in NP because a satisfying assignment serves as a polynomial-size certificate whose validity can be checked efficiently. Given a Boolean circuit with input gates and a certificate , a verifier evaluates on and accepts if the output gate evaluates to 1; this evaluation runs in time linear in the size of .[10][11] To evaluate , model it as a directed acyclic graph (DAG) where nodes are gates and edges represent wires. First, perform a topological sort of the gates in linear time, ordering them so that input gates come first, followed by gates whose inputs are earlier in the order. Then, compute gate values bottom-up: set input gates according to , and for each subsequent gate, apply its operation (AND, OR, or NOT) to the values of its predecessor gates. Each operation takes constant time, and since there are gates, the total time is .[11] Fan-out, where a gate's output connects to multiple subsequent gates, is handled without additional cost by storing or referencing the computed value once per gate. NOT gates are evaluated by simply inverting the input bit (0 to 1 or 1 to 0), ensuring no exponential blowup in computation. This process confirms the certificate satisfies if and only if the final output is 1, establishing membership in NP.[10][11]NP-Hardness and Completeness
The circuit satisfiability problem (CircuitSAT) is NP-hard because every problem in NP can be reduced to it in polynomial time. Specifically, for any language , there exists a polynomial-time verifier that accepts inputs in with a witness, and this verifier can be simulated by a Boolean circuit of polynomial size whose output gate evaluates to 1 if and only if the input is in .[9][12] A concrete illustration of this hardness comes from a polynomial-time reduction from 3SAT, a canonical NP-complete problem. In this reduction, each variable in the 3CNF formula corresponds to an input wire in the circuit, each clause is encoded as a small subcircuit computing the OR of its three literals (using NOT, AND, and OR gates for negation and conjunction), and the output gate computes the AND of all clause subcircuits; the resulting circuit is satisfiable if and only if the original formula is.[13][14] Full details of such constructions, including the general case for arbitrary NP problems, appear in the Cook-Levin theorem. Circuits provide a natural framework for these reductions compared to formulas in SAT, as they avoid the need to parse textual representations or handle variable scoping, enabling direct construction of gadgets for logical operations without additional overhead.[9][2] Since CircuitSAT is in NP—as established by the polynomial-time verifiable nature of satisfying assignments—and NP-hard, it follows that CircuitSAT is NP-complete.[9][14] CircuitSAT was introduced by Stephen Cook in 1971 alongside the Boolean satisfiability problem, with circuits chosen to simplify the foundational NP-completeness proofs by directly modeling nondeterministic computations.[9][12]Proofs of NP-Completeness
Cook-Levin Theorem
The Cook-Levin theorem establishes the NP-completeness of the circuit satisfiability problem (CircuitSAT) by providing a polynomial-time reduction from any language in NP to CircuitSAT, demonstrating that CircuitSAT is NP-hard. Specifically, for the 3SAT problem, the reduction constructs a boolean circuit that simulates the computation of a nondeterministic Turing machine (NTM) verifier for 3SAT instances, ensuring the circuit is satisfiable if and only if the original 3SAT formula is satisfiable.[9][15] The reduction simulates the NTM verifier's computation using a tableau—a T × T grid representing the machine's configuration over T time steps, where T is polynomial (O(n^k)) in the input size n of the 3SAT formula. The tableau encodes the tape contents, head position, and state at each step, with the initial row fixed to the input formula and guessed assignment, consecutive rows enforcing valid transitions, and the final row indicating acceptance if all clauses are satisfied. The simulating circuit takes as inputs the bits representing the tableau cells and uses gates to verify the constraints, outputting 1 precisely when an accepting computation exists. This construction runs in polynomial time relative to n.[9][15] Key components of the circuit include subcircuits for the TM's transition function, which enforce that each consecutive pair of tableau rows follows the machine's rules using local checks on overlapping 2×3 windows of cells (e.g., gates computing whether the current head position, state, and tape symbols determine the next correctly). Variable tracking across steps is handled by input bits for each tableau cell, connected via gates that propagate constraints between time steps without additional nondeterminism. The final acceptance check uses a subcircuit that scans the last row for the accepting state, confirming the computation halts correctly. For the 3SAT verifier, this ties into clause evaluation during simulation.[15][14] In the 3SAT context, clause satisfaction subcircuits ensure that, at the computation's end, at least one literal in each clause evaluates to true based on the assignment encoded in the initial tableau row. For a clause like (l_1 ∨ l_2 ∨ l_3), where each l_i is a literal (variable or its negation), a dedicated subcircuit computes the literal values from the assignment inputs using NOT gates where needed, then applies an OR gate (or fan-in-2 tree for larger clauses) to verify the disjunction, with the overall acceptance requiring an AND of all such outputs across clauses. These subcircuits are integrated into the tableau verification, ensuring the simulation captures formula evaluation.[9][14] The resulting circuit has polynomial size, specifically O(T^2) gates, since there are O(T^2) cells requiring O(1) gates each for local transition and consistency checks, plus O(m) additional gates for m clauses in the acceptance subcircuits, where T is polynomial in the formula size. This bounded size guarantees the reduction is efficient.[15][9] Example: Simple 1-Clause Reduction Consider a 3SAT formula with a single clause φ = (x_1 ∨ ¬x_2). The verifier NTM simulates assigning values to x_1 and x_2, then checks the clause. The tableau (simplified for brevity, assuming T=3 steps) encodes the assignment in row 1, computes literal values in intermediate rows, and verifies the OR in row 3. The corresponding circuit C has inputs x_1, x_2 (from assignment) and tableau bits (for simulation, but in direct form for this small case):- NOT gate for ¬x_2.
- OR gate with inputs x_1 and ¬x_2.
- Output is the OR (acceptance for this single clause).
Reductions from CircuitSAT
The Circuit satisfiability problem (CircuitSAT) plays a central role in establishing the NP-hardness of other problems due to its structured representation as a Boolean circuit, which facilitates modular reductions without the need to handle variable ordering or parenthesization inherent in formula-based satisfiability problems like SAT.[16] This structure allows for the composition of local gadgets corresponding to individual gates, enabling the embedding of the circuit's computation into the target problem's instance in a straightforward manner.[16] The general approach in such reductions involves translating the circuit's directed acyclic graph (DAG) into the elements of the target problem, such as vertices, edges, or constraints that enforce the logical behavior of each gate (AND, OR, NOT) and propagate truth values from inputs to outputs. For instance, in graph-based problems like 3-coloring, the circuit can be encoded by constructing a graph where node colors represent Boolean values (true or false), and edges enforce the gate semantics through coloring constraints. This method leverages the circuit's explicit wiring to avoid the exponential blowup sometimes associated with converting formulas to canonical forms. A prominent example is the reduction from CircuitSAT to the Minesweeper consistency problem, which determines whether a partially revealed Minesweeper board has a valid mine placement consistent with the given numbers. In this construction, each gate in the circuit is encoded by a local subgrid on the board, where cells represent the gate's output (open for true, mined for false), and adjacent number clues enforce the logical operation—e.g., an AND gate requires both inputs true for the output to be true, simulated by mine placements and count constraints that penalize inconsistent configurations. Mines explicitly represent falsity, and the board's global consistency ensures that input assignments propagate correctly through the circuit to satisfy the output gate if and only if the original circuit is satisfiable. This reduction demonstrates CircuitSAT's utility in proving NP-completeness for game-theoretic problems, with the polynomial-time construction preserving the satisfiability relation.[17] Other reductions illustrate the versatility of CircuitSAT, such as to the Hamiltonian path problem, where the circuit is modeled as a layered graph with one layer per circuit depth, and path segments through gate gadgets select truth values that satisfy the connections. Similarly, for vertex cover, a gadget is built for each gate to force selection of vertices corresponding to true outputs or inputs as needed to "cover" edges representing logical implications, ensuring a small vertex cover exists if and only if the circuit is satisfiable. These examples highlight the advantages of CircuitSAT: its modular gadgets compose naturally without the structural overhead of formulas, leading to more efficient and intuitive proofs of hardness.[17]Variants and Related Problems
Restricted CircuitSAT Variants
The CircuitSAT problem remains NP-complete under various structural restrictions on the underlying Boolean circuit, allowing researchers to study the robustness of its hardness and develop specialized algorithms or lower bounds for subclasses. These variants impose limits on the circuit's topology, gate types, depth, or fan-in, often to explore connections to graph theory, parallel computation, or proof complexity. One prominent restriction is planar CircuitSAT, where the circuit is required to be a planar directed acyclic graph, meaning its underlying undirected graph can be embedded in the plane without edge crossings. This variant preserves NP-completeness through a straightforward reduction from planar 3-SAT. In this reduction, each clause in the planar 3-SAT instance is encoded as a small subcircuit consisting of NOT, AND, and OR gates for literals and clause conjunction, with wires routed to respect the planarity of the variable-clause incidence graph; the overall circuit size remains polynomial, and satisfiability is equivalent. The membership in NP follows from the general case. Another key variant is bounded-depth CircuitSAT, where the circuit depth (longest path from input to output) is restricted to a constant . This problem is NP-complete for any fixed constant . For instance, 3-SAT reduces to depth-3 CircuitSAT by placing NOT gates on negated literals at depth 1, 3-input AND gates for each clause at depth 2, and a single unbounded-fan-in OR gate over all clauses at depth 3; the resulting circuit has polynomial size and is satisfiable if and only if the original formula is. For , the complexity depends on the gate arrangement: it is in P if the circuit computes a DNF formula (testable by checking for a non-empty term), but NP-complete in general (e.g., for circuits computing CNF formulas with literals). Algorithms for constant-depth CircuitSAT exploit the structure for subexponential-time solutions, such as for depth and linear size, improving on brute-force . The monotone CircuitSAT variant eliminates negation gates, using only AND and OR gates (possibly with constants). Due to the monotone (non-decreasing) nature of such circuits, the problem is in P: evaluate the circuit on the all-true input; if the output is true, it is satisfiable by that assignment; otherwise, it is unsatisfiable, as no other assignment can yield true. The related monotone circuit value problem—evaluating the output for a given input—is P-complete, highlighting the restriction's impact on evaluation rather than search. Finally, small fan-in CircuitSAT limits each gate to at most two inputs. This variant is NP-complete, as the original Cook-Levin reduction from general NP problems to CircuitSAT produces circuits with binary gates (e.g., using binary trees to simulate larger fan-ins if needed, though many verifiers use fan-in 2 directly). The restriction does not simplify the problem, as binary gates suffice to express arbitrary Boolean functions.| Variant | Complexity | Notes |
|---|---|---|
| Planar CircuitSAT | NP-complete | Hard via planar 3-SAT reduction; useful for geometric and graph problems. |
| Bounded-depth (constant ) | NP-complete | Includes 3-SAT as depth-3 case; subexponential algorithms exist. |
| Depth-2 CircuitSAT | NP-complete (general); P (DNF-like) | Depends on top/bottom gate types. |
| Monotone CircuitSAT | in P | Decided by evaluation at all-1 input; value problem is P-complete. |
| Small fan-in (≤2) | NP-complete | Standard reductions use binary gates. |
Complementary and Counting Variants
The complementary variant of the Circuit Satisfiability problem, known as Circuit-UNSAT, asks whether there exists no input assignment to a given Boolean circuit that evaluates to 1 at the output gate.[18] This problem is co-NP-complete. Membership in co-NP follows because Circuit-UNSAT is the complement of CircuitSAT, which is in NP.[16] For co-NP-hardness, a reduction from co-3SAT (the complement of 3SAT, which is co-NP-complete) proceeds by converting the 3CNF formula into an equivalent Boolean circuit in polynomial time, preserving unsatisfiability; since the formula is unsatisfiable if and only if the corresponding circuit outputs 0 for all inputs, this establishes the hardness.[18] Circuit-UNSAT is equivalent to the tautology problem for circuits, where one checks if the circuit (interpreted as a formula) is true for all inputs, and it plays a key role in proof complexity studies, such as lower bounds on proof sizes for unsatisfiability.[19] The counting variant, denoted #CircuitSAT, seeks to compute the exact number of input assignments that satisfy a given Boolean circuit, i.e., make the output evaluate to 1. This problem is #P-complete under parsimonious reductions, meaning reductions preserve the exact number of solutions.[20] To show #P-completeness, note that #CircuitSAT is in #P because the satisfying assignments can be enumerated via a nondeterministic polynomial-time machine that simulates the circuit on guessed inputs. For hardness, any #P problem reduces parsimoniously to #CircuitSAT: given a nondeterministic verifier machine for a language in NP, construct a circuit that simulates the verifier on input x and a guessed witness, counting the accepting witnesses exactly as the number of satisfying assignments.[20] Valiant established #P-completeness for related counting problems like #SAT via reductions involving the permanent function, and the parsimonious nature of circuit-to-formula conversions extends this to #CircuitSAT. #CircuitSAT relates to the probabilistic complexity class PP, where a language is in PP if there exists a probabilistic polynomial-time Turing machine that accepts with probability greater than 1/2 if the input is in the language and at most 1/2 otherwise; the decision problem of whether the number of satisfying assignments exceeds 2^{n-1} (for n inputs) is PP-complete, linking counting to probabilistic acceptance thresholds. However, the focus remains on exact counting, as approximation algorithms for #CircuitSAT, such as those using inclusion-exclusion or Markov chain Monte Carlo methods, enable efficient estimation in practice for certain circuit classes. Applications include probabilistic verification of circuit reliability (e.g., counting failure modes) and approximate model counting in automated reasoning tools.[21][22]Key Transformations
Tseytin Transformation
The Tseytin transformation converts a Boolean circuit into an equisatisfiable conjunctive normal form (CNF) formula, enabling the use of CNF-based satisfiability solvers while preserving the circuit's satisfiability semantics. This method introduces auxiliary variables for gate outputs and generates clauses that enforce each gate's logical behavior, resulting in a formula whose size is linear in the number of circuit gates.[23] Developed by G. S. Tseytin in his 1967 work on the complexity of propositional derivations, the transformation was originally motivated by studies in proof complexity but has become a foundational technique for encoding structured problems into SAT instances for modern DPLL-style solvers.[23] It produces a CNF formula that is satisfiable if and only if the original circuit can evaluate to true under some input assignment, with no exponential blowup in size.[24] To apply the transformation, a new Boolean variable is introduced for the output of each gate in the circuit. For every gate, a set of clauses is added to ensure this variable equals the gate's function applied to its input variables (or previously introduced output variables). The clauses are derived from the equisatisfiability conditions for each gate type. For binary gates like AND and OR, three clauses suffice; for unary NOT gates, two clauses are used. The complete CNF formula is the conjunction of all these gate-specific clauses across the circuit, augmented by a single unit clause asserting that the root gate's output variable is true.[25] Specifically, for an AND gate with inputs and , and output variable , the equivalence is encoded as the following clauses: For an OR gate with the same inputs and output, yields: For a NOT gate with input and output , is encoded as: These clause sets ensure the auxiliary variable faithfully represents the gate output in any satisfying assignment.[24][25] The resulting CNF has a size of , where is the number of gates, as each gate contributes a fixed number of clauses (at most three) with a constant number of literals per clause. This linear scaling makes the transformation efficient for large circuits, avoiding the potential exponential growth of naive CNF conversions.[24] As an illustration, consider a simple circuit with a single XOR gate taking inputs and , producing output , where satisfiability requires . The equivalence is encoded using four clauses: Appending the unit clause yields the full CNF formula, which is satisfiable exactly when there exists an input assignment making . This example demonstrates how the transformation handles non-standard gates like XOR via their full equisatisfiability CNF representation.[25]Circuit-to-Formula Conversions
The direct translation of a boolean circuit to a propositional formula constructs a tree-structured expression that mirrors the circuit's directed acyclic graph (DAG), with each gate mapped to a corresponding logical connective such as AND, OR, or NOT. For instance, a circuit computing would yield the formula , preserving the computational structure. However, propositional formulas lack the subformula sharing inherent in circuit DAGs; naive expansion of shared subcircuits—common in circuits for efficiency—replicates computations, leading to exponential growth in formula size relative to the circuit.[26] To mitigate this exponential blowup while retaining compactness, conversion methods introduce auxiliary variables akin to those in the Tseitin transformation, assigning new propositional variables to gates or subcircuits and adding equisatisfiability constraints. This approach contrasts sharply with naive expansion: the former yields a formula linear in the circuit size by preserving sharing through definitions like , whereas the latter duplicates subexpressions, inflating size for circuits with high fan-out or depth. The Tseytin transformation represents a specific case of this auxiliary-based strategy, optimized for CNF output.[27] Direct conversion of circuits to disjunctive normal form (DNF) or conjunctive normal form (CNF) without auxiliaries is feasible via repeated application of distributive laws but incurs exponential size in the worst case, as pushing negations and distributing connectives over large subformulas generates vastly more terms or clauses.[27] Beyond propositional formulas, circuits can be encoded as quantified Boolean formulas (QBF) to capture alternating existential and universal quantification, useful for modeling adversarial or verification scenarios where not all variables are existentially quantified. For example, in equivalence checking, a QBF might quantify outputs universally against an expected specification. Similarly, encodings to satisfiability modulo theories (SMT) extend boolean circuits into richer logics, such as bit-vector arithmetic, by mapping gates to theory-specific operations while keeping the boolean skeleton intact.[28][29] These circuit-to-formula conversions underpin applications in formal proof systems and hardware verification. In extended resolution proof systems, auxiliaries enable derivations that simulate circuit evaluations, allowing succinct refutations of unsatisfiable instances by extending the variable set with subcircuit definitions. In hardware verification, such encodings facilitate property checking via SAT or SMT solvers, translating circuit behaviors into formulas for bounded model checking or equivalence validation.[30][29]| Conversion Method | Size Relative to Circuit | Equivalence Type | Practical Solvability |
|---|---|---|---|
| Direct Tree Formula | Exponential (due to unshared expansion) | Semantically equivalent | Challenging; large size hinders SAT solvers despite direct structure.[27][26] |
| Tseitin CNF (with auxiliaries) | Linear | Equisatisfiable | Favorable; CNF format suits modern SAT solvers efficiently.[27] |