Circuit satisfiability problem

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. For instance, in the figure above, the circuit on the left can be satisfied by setting both inputs to be 1, but the circuit on the right is unsatisfiable.

CircuitSAT is closely related to Boolean satisfiability problem (SAT), and likewise, has been proven to be NP-complete.^[2] In fact, it is a prototypical NP-complete problem; the Cook–Levin theorem is sometimes proved on CircuitSAT instead of on the SAT and then 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, we'll reduce 3SAT to Circuit SAT. The reduction goes as follows:

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.

Variants

Planar Circuit SAT

Weighted Circuit SAT

Arithmetic Circuit SAT

Reduction

Arithmetization is to reduce a CircuitSAT problem into a set of arithmetic constrains. Currently, in the literature, there are two direction of reduction: reduce to a combination satisfiability problem or reduce to an algebraic satisfiability problem. An example of such reduction from boolean circuit to polynomial is presented here, and they are called Zhegalkin_polynomial.

The Tseitin transformation

There is a straightforward reduction from CircuitSAT to SAT, known as the Tseitin transformation. The transformation is especially easy to describe if the circuit is wholly constructed from 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]^[5] (The converse, that SAT is reducible to CircuitSAT, is even easier—we simply rewrite the Boolean formula as a circuit and solve that.)

References

^ ^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).
^ 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".
^ 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).

[np-complete-problems-1] 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).

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

[5] 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).

[1]

[2]

[3]

[4]

[5]