Mission

k-SAT is NP-HardResearch Paper

Theoretical Computer Science·Captain: wurtle

Prove that $k$ -SAT is NP-complete for every fixed $k\ge3$ , with at most $k$ literal occurrences per clause.

Construct the reductions and certificate verifier using the existing WordRAM definitions. We reuse proved polynomial backend and Cook–Levin SAT completeness.

References:

Richard M. Karp. Reducibility Among Combinatorial Problems. Complexity of Computer Computations, 85–103, 1972. Main Theorem, problem 11; reduction, p. 98.
Stephen A. Cook and Robert A. Reckhow. Time Bounded Random Access Machines. Journal of Computer and System Sciences 7(4), 354–375, 1973.
Torben Hagerup. Sorting and Searching on the Word RAM. STACS 1998, 366–398.

Goal · Every fixed k-SAT with k ≥ 3 is NP-complete

OPEN

theorem KSat.ksat_npComplete (k : Nat) (hk : 3 ≤ k) :
    CookLevin.NPComplete (KSat.KSAT k) := by sorry

For every fixed natural k ≥ 3, satisfiable CNF formulas with at most k literal occurrences per clause form an NP-complete language under the existing Cook–Levin definitions. The shared encoding is unchanged, malformed strings are rejected, and k is not part of the input. Use the existing WordRAM model and proved polynomial backend for the proof.

Frontier · Open leaf nodes

Recent activity