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. 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. In the figure to the right, the left circuit can be satisfied by setting both inputs to be 1, but the right circuit is unsatisfiable. 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. 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. In the figure to the right, the left circuit can be satisfied by setting both inputs to be 1, but the right circuit is unsatisfiable. CircuitSAT is closely related to Boolean satisfiability problem (SAT), and likewise, has been proven to be NP-complete. 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. The satisfiability of a circuit containing m {displaystyle m} arbitrary binary gates can be decided in time O ( 2 0.4058 m ) {displaystyle O(2^{0.4058m})} . 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, it is possible to construct a reduction from 3SAT to Circuit SAT. Suppose the original 3SAT formula has variables x 1 , x 2 , … , x n {displaystyle x_{1},x_{2},dots ,x_{n}} , and operators (AND, OR, NOT) y 1 , y 2 , … , y k {displaystyle y_{1},y_{2},dots ,y_{k}} . 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 ( ¬ x 1 ∧ x 2 ) ∨ x 3 , {displaystyle (lnot x_{1}land x_{2})lor x_{3},} the circuit will have 3 inputs, one AND, one OR, and one NOT gate. The input corresponding to x 1 {displaystyle x_{1}} will be inverted before sending to an AND gate with x 2 , {displaystyle x_{2},} and the output of the AND gate will be sent to an OR gate with x 3 . {displaystyle x_{3}.}