Satisfiability problem for circuits

In theoretical computer science (especially in complexity theory ) the satisfiability problem for circuits ( English Circuit Satisfiability Problem , CircuitSAT , CSAT ) is the decision problem as to whether there is an input for a given Boolean circuit that makes the output true.

Problem

A Boolean circuit is considered, which consists of binary AND gates, binary OR gates, unary non-gates, input gates and an output gate. It is to be decided whether an input (i.e. an assignment of truth values to the input gates) exists for which the output gate becomes true.

The selection of the allowed gates in the Boolean circuit varies in the literature. The choice of AND, OR and NOT gates allows all Boolean functions to be formed with circuits. Other variants allow, for example, additional gates for the two truth values or use NAND gates instead of the AND, OR and NOT gates.

complexity

The satisfiability problem for circuits is NP-complete . It is considered a prototypical NP-complete problem and is introduced as the first NP-complete problem in some textbooks. It can be used to prove the NP severity of other problems through reduction. In particular, there is a relatively simple reduction to the satisfiability problem of propositional logic (SAT), and CircuitSAT can therefore be used to show the NP-severity of SAT ( Cook Theorem ).

The size of a circuit is the number of gates in the circuit, not including input gates. CircuitSAT in can be chosen for a circuit with input gates . For this purpose, you can test for each of the possible inputs in polynomial time whether the output gate becomes true (see Circuit Value Problem ). ${\ displaystyle size (C)}$ ${\ displaystyle C}$ ${\ displaystyle C}$ ${\ displaystyle n}$ ${\ displaystyle O (2 ^ {n} \ cdot poly (size (C)))}$ ${\ displaystyle 2 ^ {n}}$

Depending on the circuit size, the problem can be decided in. This limit holds for circuits with any binary gates. ${\ displaystyle O (2 ^ {0.4058 \ cdot size (C)})}$

literature

Christos H. Papadimitriou : Computational Complexity . Addison-Wesley, Reading / Mass, 1995, ISBN 978-0-201-53082-7 , 4.3 Boolean functions and circuits & 8 Reductions and completeness (English).

Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , Clifford Stein : Introduction to Algorithms . Third ed. MIT Press, Cambridge, Massachusetts; London, England 2009, ISBN 978-0-262-03384-8 , 43.3 NP-completeness and reducibility - Circuit satisfiability, pp. 1070-1078 (English).

Individual evidence

↑ Sergey Nurk: An O (2 ^ {} 0.4058) upper bound for Circuit SAT . December 1, 2009.

[1] Sergey Nurk: An O (2 ^ {} 0.4058) upper bound for Circuit SAT . December 1, 2009.