Proof Sketch of Cook-Levin Theorem

wimmers / poly-reductions

Polynomial-time reductions in Isabelle/HOL

2 stars 13 forks source link

Proof Sketch of Cook-Levin Theorem #19

Closed maxhaslbeck closed 3 years ago

maxhaslbeck commented 3 years ago

write down main-lemma (not prove it)
prove Cook-Levin with main-lemma
what is left to prove that SAT is NP-complete?

maxhaslbeck commented 3 years ago

merged PR #27 sets up and proves the cook-levin theorem assuming main_lemma, that gives us that SAT is NP-hard. Furthermore, we need to prove that SAT is in NP (cf #26).