Proof of `NP-Hardness of [2,3]-Bounded 3-SAT`
groundedproofs/Lax345332Proofs/BFinal.lean · lax-345332
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
In the paper
- page 6 of this submission's paper
Description
Satisfiability is NP-hard by the Cook–Levin theorem; the reduction to (3,4)-SAT followed by the copy construction is correct and, as the composition of two polynomial-time computations, runs in polynomial time; polynomial-time many-one reductions compose.