Circuit satisfiability problem

Last updated July 03, 2023

The circuit on the left is satisfiable but the circuit on the right is not. CircuitSAT.svg — The circuit on the left is satisfiable but the circuit on the right is not.

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 $m$ arbitrary binary gates can be decided in time $O(2^{0.4058m})$ .^[4]

Proof of NP-Completeness

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 $x_{1},x_{2},\dots ,x_{n}$ , and operators (AND, OR, NOT) $y_{1},y_{2},\dots ,y_{k}$ . 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 $(\lnot x_{1}\land x_{2})\lor x_{3},$ the circuit will have 3 inputs, one AND, one OR, and one NOT gate. The input corresponding to $x_{1}$ will be inverted before sending to an AND gate with $x_{2},$ and the output of the AND gate will be sent to an OR gate with $x_{3}.$

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

Planar Circuit SAT

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

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

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

This problem asks whether it is possible to locate all the bombs given a Minesweeper board. It has been proven to be CoNP-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

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 (v₁ ∨ v₃) ∧ (v₂ ∨ v₃) ∧ (¬v₁ ∨ ¬v₂ ∨ ¬v₃), where v₁ and v₂ are the inputs to the NAND gate and v₃ 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.

Related Research Articles

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

In computational complexity theory, co-NP is a complexity class. A decision problem X is a member of co-NP if and only if its complement X is in the complexity class NP. The class can be defined as follows: a decision problem is in co-NP if and only if for every no-instance we have a polynomial-length "certificate" and there is a polynomial-time algorithm that can be used to verify any purported certificate.

The #P-complete problems form a complexity class in computational complexity theory. The problems in this complexity class are defined by having the following two properties:

In computational complexity theory, a decision problem is P-complete if it is in P and every problem in P can be reduced to it by an appropriate reduction.

In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP-complete, 2-satisfiability can be solved in polynomial time.

In computer science, parameterized complexity is a branch of computational complexity theory that focuses on classifying computational problems according to their inherent difficulty with respect to multiple parameters of the input or output. The complexity of a problem is then measured as a function of those parameters. This allows the classification of NP-hard problems on a finer scale than in the classical setting, where the complexity of a problem is only measured as a function of the number of bits in the input. This appears to have been first demonstrated in Gurevich, Stockmeyer & Vishkin (1984). The first systematic work on parameterized complexity was done by Downey & Fellows (1999).

In computational complexity theory, the Cook–Levin theorem, also known as Cook's theorem, states that the Boolean satisfiability problem is NP-complete. That is, it is in NP, and any problem in NP can be reduced in polynomial time by a deterministic Turing machine to the Boolean satisfiability problem.

In computational complexity theory, a function problem is a computational problem where a single output is expected for every input, but the output is more complex than that of a decision problem. For function problems, the output is not simply 'yes' or 'no'.

In Boolean algebra, any Boolean function can be expressed in the canonical disjunctive normal form (CDNF) or minterm canonical form, and its dual, the canonical conjunctive normal form (CCNF) or maxterm canonical form. Other canonical forms include the complete sum of prime implicants or Blake canonical form, and the algebraic normal form.

In complexity theory, the Karp–Lipton theorem states that if the Boolean satisfiability problem (SAT) can be solved by Boolean circuits with a polynomial number of logic gates, then

The Valiant–Vazirani theorem is a theorem in computational complexity theory stating that if there is a polynomial time algorithm for Unambiguous-SAT, then NP = RP. It was proven by Leslie Valiant and Vijay Vazirani in their paper titled NP is as easy as detecting unique solutions published in 1986. The proof is based on the Mulmuley–Vazirani–Vazirani isolation lemma, which was subsequently used for a number of important applications in theoretical computer science.

MAX-3SAT is a problem in the computational complexity subfield of computer science. It generalises the Boolean satisfiability problem (SAT) which is a decision problem considered in complexity theory. It is defined as:

In computational complexity theory, the maximum satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula. It is a generalization of the Boolean satisfiability problem, which asks whether there exists a truth assignment that makes all clauses true.

In computational complexity theory and circuit complexity, a Boolean circuit is a mathematical model for combinational digital logic circuits. A formal language can be decided by a family of Boolean circuits, one circuit for each possible input length.

In computational complexity theory, a gadget is a subunit of a problem instance that simulates the behavior of one of the fundamental units of a different computational problem. Gadgets are typically used to construct reductions from one computational problem to another, as part of proofs of NP-completeness or other types of computational hardness. The component design technique is a method for constructing reductions by using gadgets.

In computational complexity theory, the language TQBF is a formal language consisting of the true quantified Boolean formulas. A (fully) quantified Boolean formula is a formula in quantified propositional logic where every variable is quantified, using either existential or universal quantifiers, at the beginning of the sentence. Such a formula is equivalent to either true or false. If such a formula evaluates to true, then that formula is in the language TQBF. It is also known as QSAT.

In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula $is satisfiable because it is true when and, while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not.$

In computer science, the Sharp Satisfiability Problem is the problem of counting the number of interpretations that satisfy a given Boolean formula, introduced by Valiant in 1979. In other words, it asks in how many ways the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. For example, the formula $is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments, ,, we have$

The Tseytin transformation, alternatively written Tseitin transformation, takes as input an arbitrary combinatorial logic circuit and produces a boolean formula in conjunctive normal form (CNF), which can be solved by a CNF-SAT solver. The length of the formula is linear in the size of the circuit. Input vectors that make the circuit output "true" are in 1-to-1 correspondence with assignments that satisfy the formula. This reduces the problem of circuit satisfiability on any circuit to the satisfiability problem on 3-CNF formulas. It was discovered by the Russian scientist Grigori Tseitin.

In computer science, the planar 3-satisfiability problem (abbreviated PLANAR 3SAT or PL3SAT) is an extension of the classical Boolean 3-satisfiability problem to a planar incidence graph. In other words, it asks whether the variables of a given Boolean formula—whose incidence graph consisting of variables and clauses can be embedded on a plane—can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

References

1 2 3 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.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[np-complete-problems-1] 1 2 3 David Mix Barrington and Alexis Maciel (July 5, 2000). "Lecture 7: NP-Complete Problems" (PDF).

[2] 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.

[3] See also, for example, the informal proof given in Scott Aaronson's lecture notes from his course Quantum Computing Since Democritus.

[4] Sergey Nurk (December 1, 2009). "An O(2^{0.4058m}) upper bound for Circuit SAT".

[:0-5] "Algorithmic Lower Bounds: Fun With Hardness Proofs at MIT" (PDF).

[6] 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.

[7] Kaye, Richard (Mar 2000). "Minesweeper is NP-complete" (PDF). The Mathematical Intelligencer. 22 (2): 9–15. doi:10.1007/BF03025367. S2CID 122435790.

[8] see File:Crossover xor.gif and File:Crossover nand.pdf

[9] 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.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]