Advisors: Fabian Kunze
In this thesis, we formally verify a proof of the Cook-Levin-Theorem in the proof assistant Coq. The Cook-Levin Theorem states that the satisfiability problem SAT of conjunctive normal forms is NP-complete. This means that any language which is polynomial-time verifiable is reducible to SAT in polynomial time.
The theorem was proved in 1971 by Stephen A. Cook [1] and was independently discovered by Leonid Levin in 1973 [2]. Since the subsequent discovery of more NP-complete problems by Richard Karp in 1972 [3], it has become one of the most important results of modern computational complexity theory. Despite its importance, most proofs do not even attempt to verify the construction's correctness.
For the proof, one has to encode computations of a chosen reasonable computational model using Boolean formulas. We use the call-by-value λ-calculus L as the computational model, which has been shown to be polynomial-time and linear-space equivalent to Turing machines [4]. It is much easier to write and verify L programs than to program Turing machines. Thus, we need to reduce the computation of L formulas to SAT. However, Turing machines are structurally simpler than the λ-calculus and we therefore propose to use Turing machines as an intermediate problem in the reduction of L to SAT.
In this work, we introduce the basics of formalising polynomial-time reductions in Coq. We present a polynomial-time reduction from Turing machines to SAT which is based on the original tableau construction by Cook and formally verify its correctness. The original construction is adapted and factorised in order to make a formal proof feasible. We see this as a significant first step towards showing SAT to be NP-complete in L.