Circuit satisfiability problem: Difference between revisions

Revision as of 02:40, 16 April 2019

Revision as of 02:55, 16 April 2019

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> In other words, it asks whether the inputs to a given Boolean Circuit can be consistently set to '''1''' or '''0''' such that the circuit outputs '''1'''. If that is the case, the circuit is called ''satisfiable''. Otherwise, the circuit is called ''unsatisfiable.'' This problem is closely related to [[Boolean satisfiability problem|Boolean satisfiability problem (SAT)]], and likewise, 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 the [[Boolean satisfiability problem|SAT]] 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>

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