Circuit satisfiability problem

In <a href="/facts/Theoretical_computer_science/jSkGGuvy">theoretical computer science</a>, the circuit satisfiability problem (also known as CIRCUIT-SAT, CircuitSAT, CSAT, etc.) is the <a href="/facts/Decision_problem/cQNWjbdE">decision problem</a> of determining whether a given <a href="/facts/Boolean_circuit/TwhfJp0q">Boolean circuit</a> 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 <a href="/facts/Boolean_satisfiability_problem/wBVRjWoy">Boolean satisfiability problem (SAT)</a>, and likewise, has been proven to be <a href="/facts/NP-complete/NFPv56DU">NP-complete</a>. It is a prototypical NP-complete problem; the <a href="/facts/Cook%25E2%2580%2593Levin_theorem/6WN3aUyL">Cook–Levin theorem</a> 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. 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})}
 
.

Circuit satisfiability problem open-in-new

Circuit satisfiability problem