3-SAT a specidal case of the boolean satsifiability problem
A) 3-SAT
B) NP
a formula is satisfiable if there exists (at least) one bitstring such that q = 1
boolean satisfiability problems asks whether a given k-CNF is satisfiabel
k-SAT
A) k-CNF
B) satisfiable
the maximum clause size k >= k in a CNF can be reduced to 3 at the cost of extra variables and extra clauses
1-SAT, 2-SAT in P
3-SAT -> NP , if we can solve 3-SAT every other problem in NP with only polynomial overhead
Cook-levin theorem
A) NP
B) 3-SAT
C) polynomially
Universality of elementary logical operations
A) l
B) l-CNF
C) 2^l
A TM operates in steps, where each step only involves a very restricted set of operations. Every such step can only affect the internal state register. TM computations are highly local
Instead of presenting the logical functionality of a verification procedure as a single huge CNF, we should try to represent the actual TM computation by a sequence of small boolean formulas .
The two features (polynomial runnnig time, locality of TMs) allow for transforming entire TM computations into a single CNF formula, requirements :
initialization
termination
consistent computation
Polynomial number of 3-CNFs
A) input
B) consistency
C) termination
Visualization of a cook-leving bitstring encoding
A) input x
B) input y
C) internal states & tape changes
D) accept
The Cook-levin theorem is also a good example for the power of abstraction. The statement itself holds regardless of the underlying computational model.
