Circuit satisfiability problem: Difference between revisions

Revision as of 19:16, 8 May 2019

Revision as of 19:18, 8 May 2019

Line 1:

[[File:CircuitSAT.svg|thumb|The circuit on the left is satisfiable but the circuit on the right is not.|341x341px]]

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.'' For instance, inIn the figure above,to the circuit onright, the left circuit can be satisfied by setting both inputs to be '''1''', but the right circuit on the right is unsatisfiable.

CircuitSAT 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> It is a prototypical NP-complete problem; the [[Cook–Levin theorem]] is sometimes proved on CircuitSAT instead of on the 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> The satisfiability of a circuit containing <math>m</math> 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>

==Proof of NP-Completeness==

Given a circuit and a satisfying set of inputs, one can compute the output of each gate in constant time. Hence, the output of the circuit is verifiable in polynomial time. Thus Circuit SAT belongs to complexity class NP. To show [[NP-hardness]], we'llit is possible to reduce from [[3SAT]] to Circuit SAT. The reduction goes as follows:

Suppose the original 3SAT formula has variables <math>x_1,x_2,\dots,x_n</math>, and operators (AND, OR, NOT) <math>y_1,y_2,\dots,y_k</math>. Design a circuit such that it has an input corresponding to every variable and a gate corresponding to every operator. Connect the gates according to the 3SAT formula. For instance, if the 3SAT formula is <math>(\lnot x_1\land x_2)\lor x_3,</math>the circuit will have 3 inputs, one AND, one OR, and one NOT gate. The input corresponding to <math>x_1</math>will be inverted before sending to an AND gate with <math>x_2,</math>and the output of the AND gate will be sent to an OR gate with <math>x_3.</math>