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 (v1 ∨ v3) ∧ (v2 ∨ v3) ∧ (¬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.[4][1] (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
- ^ 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).
{{cite web}}: Check date values in:|date=(help) - ^ See also, for example, the informal proof given in Scott Aaronson's lecture notes from his course Quantum Computing Since Democritus.
- ^ 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).
- ^ Sergey Nurk (December 1, 2009). "An O(2^{0.4058m}) upper bound for Circuit SAT".