Circuit satisfiability problem: Difference between revisions

Revision as of 10:38, 5 November 2012

Revision as of 16:00, 6 February 2013

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 [[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 name="np-complete-problems" /><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|dateyear=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.)

The satisfiability of a circuit containing m arbitrary binary gates can be decided in time O(2^{0.4058m}) .<ref>{{cite web|url=http://www.pdmi.ras.ru/preprint/2009/09-10.html|title=An O(2^{0.4058m}) upper bound for Circuit SAT|author=Sergey Nurk|date=December 1, 2009}}</ref>.

== References ==

Line 12:

== See also ==

* [[Satisfiability problem]]

{{comp-sci-theory-stub}}

[[Category:NP-complete problems]]

[[Category:Computational problems]]

[[Category:Computability theory]]

{{comp-sci-theory-stub}}