# Circuit satisfiability problem

(Redirected from Circuit satisfiability)

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]

CircuitSAT 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 SAT for Boolean expressions and then reduced to the other satisfiability problems to prove their NP-completeness.[1][3]

There is a straightforward reduction from CircuitSAT with 2-input NAND gates (a functionally-complete set of Boolean operators) to SAT: assign every net in the circuit a variable, then replace every NAND gate with inputs v1 and v2 and output v3 with the conjunctive normal form clauses (v1v3) ∧ (v2v3) ∧ (¬v1 ∨ ¬v2 ∨ ¬v3). These clauses completely describe the relationship between the three variables. Adding 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 of the original problem.[1][4] (The converse, that SAT is reducible to CircuitSAT, is even easier—we simply rewrite the Boolean formula as a circuit and solve that.)

The satisfiability of a circuit containing m arbitrary binary gates can be decided in time $O(2^{0.4058m})$.[5]

## References

1. ^ a b c David Mix Barrington and Alexis Maciel (July 5, 2000). "Lecture 7: NP-Complete Problems".
2. ^ Luca Trevisan (November 29. 2001). "Notes for Lecture 23: NP-completeness of Circuit-SAT".
3. ^ See also, for example, the informal proof given in Scott Aaronson's lecture notes from his course Quantum Computing Since Democritus.
4. ^ 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".
5. ^ Sergey Nurk (December 1, 2009). "An O(2^{0.4058m}) upper bound for Circuit SAT".