Circuit satisfiability problem

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.[1]

Properties

CircuitSAT has been proven to be NP-complete.[2] In fact, it is a prototypical NP-complete problem; the Cook–Levin theorem is sometimes proved on CircuitSAT instead of on SAT for Boolean expressions and then reduced to the other satisfiability problems to prove their NP-completeness.[1][3]

The satisfiability of a circuit containing m arbitrary binary gates can be decided in time .[4]

The 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 functionally-complete set of Boolean operators): assign every net in the circuit a variable, then for each NAND gate, construct the conjunctive normal form clauses (v1 ∨ v3) ∧ (v2 ∨ v3) ∧ (¬v1 ∨ ¬v2 ∨ ¬v3) where v1 and v2 are the inputs to the NAND gate and v3 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.[1][5] (The converse, that SAT is reducible to CircuitSAT, is even easier—we simply rewrite the Boolean formula as a circuit and solve that.)

References

  1. 1 2 3 David Mix Barrington and Alexis Maciel (July 5, 2000). "Lecture 7: NP-Complete Problems" (PDF).
  2. ↑ Luca Trevisan (November 29, 2001). "Notes for Lecture 23: NP-completeness of Circuit-SAT" (PDF).
  3. ↑ See also, for example, the informal proof given in Scott Aaronson's lecture notes from his course Quantum Computing Since Democritus.
  4. ↑ Sergey Nurk (December 1, 2009). "An O(2^{0.4058m}) upper bound for Circuit SAT".
  5. ↑ Marques-Silva, João P. and Luís Guerra e Silva (1999). "Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning" (PDF).

See also

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.