wimmers / poly-reductions

Polynomial-time reductions in Isabelle/HOL
2 stars 13 forks source link

Reduction from SAT to 3-SAT #5

Open wimmers opened 4 years ago

wimmers commented 4 years ago

Strictly speaking, this is at the root of Karp's 21, while we so far only started from 3-SAT. We also do not strictly need this to complete Cook-Levin but it is necessary to make our Zoo meaningful.