Circuit satisfiability problem: Difference between revisions

Revision as of 04:15, 16 April 2019

Latest revision as of 17:15, 11 June 2025

(33 intermediate revisions by 20 users not shown)

Line 1:

{{Short description|Classic NP-complete problem in computer science}}

[[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 '''Circuitcircuit Satisfiabilitysatisfiability Problemproblem''' (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 Circuitcircuit 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|access-date=February 4, 2012|archive-date=December 26, 2011|archive-url=https://web.archive.org/web/20111226032218/http://www.cs.berkeley.edu/~luca/cs170/notes/lecture22.pdf|url-status=dead}}</ref> In fact, itIt is a prototypical NP-complete problem; the [[Cook–Levin theorem]] is sometimes proved on CircuitSAT instead of on the SAT, and then CircuitSAT can be 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-Completenesscompleteness==

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 reduceis possible to construct a [[reduction (complexity)|reduction]] 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>

Notice that the 3SAT formula is equivalent to the circuit designed above, hence their output is same for same input. Hence, If the 3SAT formula has a satisfying assignment, then the corresponding circuit will output 1, and vice versa. So, this is a valid reduction, and Circuit SAT is NP-hard.

This completes the proof that Circuitcircuit SAT is NP-Complete.

== VariantsRestricted variants and Relatedrelated Problemsproblems ==

=== Planar Circuitcircuit SAT ===

Assume that we are given a planar booleanBoolean circuit (i.e. a booleanBoolean circuit whose underlying graph is [[Planar graph|planar]]) containing only [[NAND gate|NAND]] gates with exactly two inputs. Planar Circuit SAT is the decision problem of determining whether this circuit has an assignment of its inputs that makes the output true. This problem is NP-complete. Moreover, if the restrictions are changed so that any gate in the circuit is a [[NOR gate|NOR]] gate, the resulting problem remains NP-complete.<ref name=":0">{{Cite web|url=http://courses.csail.mit.edu/6.892/spring19/scribe/lec6.pdf|title=Algorithmic Lower Bounds: Fun With Hardness Proofs at MIT|last=|first=|date=|website=|archive-url=|archive-date=|dead-url=|access-date=}}</ref> In fact, if the restrictions are changed so that any gate in the circuit is a [[NOR gate|NOR]] gate, the resulting problem remains NP-complete.<ref name=":0" />

=== Weighted Circuit SATUNSAT ===

Circuit UNSAT is the decision problem of determining whether a given Boolean circuit outputs false for all possible assignments of its inputs. This is the complement of the Circuit SAT problem, and is therefore [[co-NP-complete]].

==Reduction from CircuitSAT==

=== Arithmetic Circuit SAT ===

Reduction from CircuitSAT or its variants can be used to show NP-hardness of certain problems, and provides us with an alternative to dual-rail and binary logic reductions. The gadgets that such a reduction needs to construct are:

=== Circuit UNSAT ===

* A wire gadget. This gadget simulates the wires in the circuit.

==Reduction==

* A split gadget. This gadget guarantees that all the output wires have the same value as the input wire.

* Gadgets simulating the gates of the circuit.

* A true terminator gadget. This gadget is used to force the output of the entire circuit to be true.

* A turn gadget. This gadget allows us to redirect wires in the right direction as needed.

* A crossover gadget. This gadget allows us to have two wires cross each other without interacting.

=== Minesweeper Inferenceinference Problemproblem ===

Arithmetization is to reduce a CircuitSAT problem into a set of arithmetic constrains. Currently, in the literature, there are two direction of reduction: reduce to a combination satisfiability problem or reduce to an algebraic satisfiability problem. An example of such reduction from boolean circuit to polynomial is presented [[IP_(complexity)##SAT_is_a_member_of_IP|here]], and they are called [[Zhegalkin_polynomial]].

This problem asks whether it is possible to locate all the bombs given a [[Minesweeper (video game)|Minesweeper]] board. It has been proven to be [[co-NP-complete]] via a reduction from circuit UNSAT problem.<ref>{{Cite journal|last1=Scott|first1=Allan|last2=Stege|first2=Ulrike|last3=van Rooij|first3=Iris|date=2011-12-01|title=Minesweeper May Not Be NP-Complete but Is Hard Nonetheless|journal=The Mathematical Intelligencer|language=en|volume=33|issue=4|pages=5–17|doi=10.1007/s00283-011-9256-x|s2cid=122506352 |issn=1866-7414}}</ref> The gadgets constructed for this reduction are: wire, split, AND and NOT gates and terminator.<ref>{{cite journal | url=http://www.minesweeper.info/articles/MinesweeperIsNPComplete.pdf | last=Kaye|first=Richard | title=Minesweeper is NP-complete | journal=The Mathematical Intelligencer | volume=22 | number=2 | pages=9&ndash;15 | date=Mar 2000 | doi=10.1007/BF03025367| s2cid=122435790}}</ref> There are three crucial observations regarding these gadgets. First, the split gadget can also be used as the NOT gadget and the turn gadget. Second, constructing AND and NOT gadgets is sufficient, because together they can simulate the universal NAND gate. Finally, since three NANDs can be composed intersection-free to implement an XOR, and since XOR is enough to build a crossover,<ref>see [[:File:Crossover xor.gif]] and [[:File:Crossover nand.pdf]]</ref> this gives us the needed crossover gadget.

===The TseitinTseytin transformation===

{{main|TseitinTseytin transformation}}

ThereThe [[Tseytin transformation]] is a straightforward reduction from CircuitSATCircuit-SAT to SAT, known as the [[TseitinBoolean transformationsatisfiability problem|SAT]]. The transformation is especially easy to describe if the circuit is wholly constructed fromout of 2-input [[Sheffer stroke|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|url-status=dead|archive-url=https://web.archive.org/web/20220702105658/http://vinci.inesc.pt/~lgs/docs/iwls99.pdf|archive-date=2022-07-02}}</ref> (The converse, thatconverse—that SAT is reducible to CircuitSAT,circuit-SAT—follows is even easier—wetrivially simplyby rewriterewriting the Boolean formula as a circuit and solvesolving thatit.)

==See Alsoalso==

=== Minesweeper Inference Problem ===

*[[Circuit value problem]]

This problem asks whether it is possible to locate all the bombs given a [[Minesweeper (video game)|Minesweeper]] board. It has been proven to be [[Co-NP-complete|CoNP-Complete]] via a reduction from Circuit UNSAT problem.<ref>{{Cite journal|last=Scott|first=Allan|last2=Stege|first2=Ulrike|last3=van Rooij|first3=Iris|date=2011-12-01|title=Minesweeper May Not Be NP-Complete but Is Hard Nonetheless|url=https://doi.org/10.1007/s00283-011-9256-x|journal=The Mathematical Intelligencer|language=en|volume=33|issue=4|pages=5–17|doi=10.1007/s00283-011-9256-x|issn=1866-7414}}</ref>

* Structured circuit satisfiability

==See Also==

* Circuit Value Problem

* Structured Circuit Satisfiability

* [[Satisfiability problem]]

== References ==

{{reflist}}

[[Category:NP-complete problems]]