Content deleted Content added
m WP:CHECKWIKI error #61 fixed + general fixes using AWB (8884) |
No edit summary |
||
Line 5:
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<sub>1</sub>'' and ''v<sub>2</sub>'' and output ''v<sub>3</sub>'' with the [[conjunctive normal form]] clauses (''v<sub>1</sub>'' ∨ ''v<sub>3</sub>'') ∧ (''v<sub>2</sub>'' ∨ ''v<sub>3</sub>'') ∧ (¬''v<sub>1</sub>'' ∨ ¬''v<sub>2</sub>'' ∨ ¬''v<sub>3</sub>''). 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|year=1999}}</ref> (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 <math>O(2^{0.4058m})</math>.<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 ==
| |||