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.
CircuitSAT is closely related to Boolean satisfiability problem (SAT), and likewise, has been proven to be NP-complete.
[2] It 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.
[4] Given a circuit and a satisfying set of inputs, one can compute the output of each gate in constant time.
Thus Circuit SAT belongs to complexity class NP.
To show NP-hardness, it is possible to construct a reduction from 3SAT to Circuit SAT.
Design a circuit such that it has an input corresponding to every variable and a gate corresponding to every operator.
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.
Assume that we are given a planar Boolean circuit (i.e. a Boolean circuit whose underlying graph is planar) containing only NAND gates with exactly two inputs.
The gadgets that such a reduction needs to construct are: This problem asks whether it is possible to locate all the bombs given a Minesweeper board.
It has been proven to be CoNP-Complete via a reduction from Circuit UNSAT problem.
[6] The gadgets constructed for this reduction are: wire, split, AND and NOT gates and terminator.
Second, constructing AND and NOT gadgets is sufficient, because together they can simulate the universal NAND gate.
The Tseytin transformation is a straightforward reduction from Circuit-SAT to SAT.
The transformation is easy to describe if the circuit is wholly constructed out of 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.
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][9] The converse—that SAT is reducible to Circuit-SAT—follows trivially by rewriting the Boolean formula as a circuit and solving it.
