Circuit satisfiability problem: Difference between revisions

Revision as of 07:20, 8 October 2012

Revision as of 15:16, 2 November 2012

Line 3:

CircuitSAT has been proven to be [[NP-complete]].<ref>{{cite web|url=http://www.cs.berkeley.edu/~luca/cs170/notes/lecture22.pdf|title=Notes for Lecture 23: NP-completeness of Circuit-SAT|author=Luca Trevisan|date=November 29. 2001}}</ref> In fact, it is a prototypical NP-complete problem; the [[Cook–Levin theorem]] is sometimes proved on CircuitSAT instead of on [[Boolean satisfiability problem|SAT for Boolean expressions]] and then reduced to the other satisfiability problems to prove their NP-completeness.<ref name="np-complete-problems" /><ref>See also, for example, the informal proof given in [[Scott Aaronson]]'s [http://www.scottaaronson.com/democritus/lec6.html lecture notes] from his course ''Quantum Computing Since Democritus''.</ref>

There is a straightforward reduction from CircuitSAT with 2-input NAND gates (a [[Functional completeness|functionally-complete]] set of Boolean operators) to [[3-Satisfiability Problem|SAT]]: assign every [[Netlist|net]] in the circuit a variable, then replace every NAND gate with inputs ''v₁'' and ''v₂'' and output ''v₃'' with the [[conjunctive normal form]] clauses (''v₁'' ∨ ''v₃'') ∧ (''v₂'' ∨ ''v₃'') ∧ (¬''v₁'' ∨ ¬''v₂'' ∨ ¬''v₃''). 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.<ref>{{cite web|url=http://reference.kfupm.edu.sa/content/a/l/algorithms_for_satisfiability_in_combina_410353.pdf|title=Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning|author=Marques-Silva, João P. and Luís Guerra e Silva|date=1999}}</ref><ref name="np-complete-problems" /> (The converse, that SAT is reducible to CircuitSAT, is even easier—we simply rewrite the Boolean formula as a circuit and solve that.)

== References ==