Circuit satisfiability problem: Difference between revisions

Revision as of 12:50, 17 February 2014

Revision as of 14:18, 20 December 2014

Line 1:

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.<ref name="np-complete-problems">{{cite web|url=http://people.clarkson.edu/~alexis/PCMI/Notes/lectureB07.pdf|title=Lecture 7: NP-Complete Problems|date=July 5, 2000|author=David Mix Barrington and Alexis Maciel}}</ref>

==Properties==

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>

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>

==The Tseitin transformation==

{{main|Tseitin transformation}}

There is a straightforward reduction from CircuitSAT to SAT, known as the [[Tseitin transformation]]. The transformation is especially easy to describe if the circuit is wholly constructed from 2-input NAND gates (a [[Functional completeness|functionally-complete]] set of Boolean operators): assign every [[Netlist|net]] in the circuit a variable, then for each NAND gate, construct the [[conjunctive normal form]] clauses (''v₁'' ∨ ''v₃'') ∧ (''v₂'' ∨ ''v₃'') ∧ (¬''v₁'' ∨ ¬''v₂'' ∨ ¬''v₃'') where ''v₁'' and ''v₂'' are the inputs to the NAND gate and ''v₃'' is the output. These clauses completely describe the relationship between the three variables. Conjoining the clauses from all the gates with 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 to the original problem of finding inputs that make the circuit output 1.<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 ==

Line 16 ⟶ 19:

[[Category:Computational problems]]

[[Category:Computability theory]]

{{comp-sci-theory-stub}}