Reduction: Any problem in NP → SAT
All problems in NP can be reduced to a generalization of SAT which we call CIRCUIT SAT
In circuit SAT we are given a circuit, a DAG whose vertices are gates of five different types
- AND gate and OR gates have indegree 2
- NOT gates have indegree 1
- Known input gates have no incoming edges and are labeled false or true
- Unknown input gates have no incoming edges and are labeled “?”
One of the sinks of the DAG is designated as the output gate
Given an assignment of values to the unknown inputs, we can evaluate the gates of the true circuit in topological order, using the rules of Boolean logic.
Then CIRCUIT SAT is the search problem:
- Given a circuit, find a truth assignment for the unknown inputs such that the output gate evaluates to true, or report that no such assignment exists.
- It’s a generalization of SAT ⇒ SAT only requires a much simpler structure
But also: CIRCUIT SAT can be reduced to SAT
So now ALL search problems reduce to CIRCUIT SAT:
Suppose is a problem in
- Every solution to it can quickly be checked
- There is an algorithm that checks, given an instance and proposed solution , whether or not is a solution of .
-
- In DPV 7.7, we stated that any polynomial algorithm can be rendered as a circuit, whose input gates encode the input to the algorithm
- Naturally, for any input length the circuit will be scaled to the appropriate number of inputs, but total number of gates of the circuit will be polynomial in the number of inputs
- Basically we construct the algorithm to be a SAT circuit, and by DPV 7.7 the # of gates would be polynomial, and the output gate should be the output of
- So we conclude that, given any instance of problem , we can construct in polynomial time a circuit whose known inputs are the bits of , and whose unknown inputs are the bits of , such that the output is true iff the unknown inputs spell a solution of
- In other words, the satisfying truth assignments to the unknown inputs of the circuit are in one-to-one correspondence with the solutions of instance of .