Circuit satisfiability problem: Difference between revisions

Revision as of 15:16, 2 November 2012

Revision as of 10:38, 5 November 2012

Line 4:

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>{{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.)

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 ==