wimmers / poly-reductions

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

Finish the reduction from 3-SAT or SAT to 0-1 integer programming #4

Open wimmers opened 4 years ago

wimmers commented 4 years ago

Besides #3, this is the last remaining piece of Karp's 21 problems. The classic reduction seems to be from SAT directly but we have already broken with this tradition already for other reductions. Furthermore, we will need the reduction SAT <= 3-SAT anyway (see #5 ).