NP-Hardness of [2,3]-Bounded 3-SAT
Lax345332.TwoThreeSat · concepts/Lax345332/TwoThreeSat.lean · lax-345332
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
[2,3]-bounded 3-SAT asks whether a formula is satisfiable, where every clause has two or three literals and every literal, a variable together with a sign, occurs at most twice. A variable therefore occurs at most twice positively and at most twice negatively, so in at most four clauses. The problem is NP-hard: every language in NP has a polynomial-time many-one reduction to it.
Tovey's paper states its theorem for (3,4)-SAT (). This is the variant that the scheduling reductions start from, and it follows from the (3,4) case by one more reduction, given in .
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
In the paper
- page 2 of this submission's paper
Lean source view on GitHub
| 1 | import Lax345332.ThreeFourSat |
| 2 | import Mathlib.Data.List.FinRange |
| 3 | import Mathlib.Data.Nat.Bits |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: NP-Hardness of [2,3]-Bounded 3-SAT |
| 8 | type: theorem |
| 9 | --- |
| 10 | *[2,3]-bounded 3-SAT* asks whether a formula is satisfiable, where every clause has two or |
| 11 | three literals and every literal, a variable together with a sign, occurs at most twice. |
| 12 | A variable therefore occurs at most twice positively and at most twice negatively, so in at |
| 13 | most four clauses. The problem is NP-hard: every language in NP has a polynomial-time |
| 14 | many-one reduction to it. |
| 15 | |
| 16 | Tovey's paper states its theorem for (3,4)-SAT (`ThreeFourSat`). This is the variant that |
| 17 | the scheduling reductions start from, and it follows from the (3,4) case by one more |
| 18 | reduction, given in `Copies`. |
| 19 | |
| 20 | # Formalization Notes |
| 21 | |
| 22 | The definitions are those of the FairRIS submission, copied so that the two problems are |
| 23 | literally the same: clauses of two literals and clauses of three literals are separate |
| 24 | families, because the constructions that consume such a formula treat them differently. |
| 25 | |
| 26 | A formula is written as a binary word in the self-delimiting code of the scheduling |
| 27 | submissions: a number is its binary digits preceded by their count in unary. This is not |
| 28 | the unary code of the Cook–Levin submission that `SAT34` uses, and the theorem is stated |
| 29 | for the words the scheduling submissions read. |
| 30 | |
| 31 | The language only contains formulas with at most as many variables as literal positions. |
| 32 | This excludes nothing from a formula in which every variable occurs. It is needed because |
| 33 | the number of variables is written in binary: a word could name exponentially many |
| 34 | variables without using them, and a reduction that writes something for each one could not |
| 35 | run in polynomial time. |
| 36 | |
| 37 | The occurrence bound is part of the formula, as a proof that each literal occupies at most |
| 38 | two of the positions inside the clauses. |
| 39 | -/ |
| 40 | |
| 41 | namespace Lax345332.TwoThreeSat |
| 42 | |
| 43 | open Lax434930.PolynomialTime Lax434930.NondeterministicPolynomialTime |
| 44 | |
| 45 | /-- A natural number as a binary word: its digits, least significant first, preceded by |
| 46 | their number in unary. -/ |
| 47 | def encodeNat (n : ℕ) : Word := |
| 48 | List.replicate n.bits.length true ++ [false] ++ n.bits |
| 49 | |
| 50 | /-- A **[2,3]-bounded 3-SAT formula** over `vars` variables: `twoClauses` clauses of two |
| 51 | literals and `threeClauses` clauses of three literals, in which every literal — a variable |
| 52 | together with a sign — occupies at most two of the positions of the formula. -/ |
| 53 | structure Formula where |
| 54 | /-- The number of variables. -/ |
| 55 | vars : ℕ |
| 56 | /-- The number of clauses of two literals. -/ |
| 57 | twoClauses : ℕ |
| 58 | /-- The number of clauses of three literals. -/ |
| 59 | threeClauses : ℕ |
| 60 | /-- The literals of the clauses of two literals. -/ |
| 61 | aLit : Fin twoClauses → Fin 2 → Fin vars × Bool |
| 62 | /-- The literals of the clauses of three literals. -/ |
| 63 | bLit : Fin threeClauses → Fin 3 → Fin vars × Bool |
| 64 | /-- Every literal occurs at most twice in the formula. -/ |
| 65 | occ_le_two : ∀ l : Fin vars × Bool, |
| 66 | (Finset.univ.filter fun o : (Fin twoClauses × Fin 2) ⊕ (Fin threeClauses × Fin 3) => |
| 67 | Sum.elim (fun q => aLit q.1 q.2) (fun q => bLit q.1 q.2) o = l).card ≤ 2 |
| 68 | |
| 69 | namespace Formula |
| 70 | |
| 71 | variable (φ : Formula) |
| 72 | |
| 73 | /-- An assignment of a truth value to every variable. -/ |
| 74 | abbrev Assignment := Fin φ.vars → Bool |
| 75 | |
| 76 | /-- The assignment `a` satisfies `φ`: every clause, of two or of three literals, contains a |
| 77 | literal that `a` makes true. -/ |
| 78 | def Satisfies (a : φ.Assignment) : Prop := |
| 79 | (∀ c, ∃ α, a (φ.aLit c α).1 = (φ.aLit c α).2) ∧ |
| 80 | (∀ c, ∃ α, a (φ.bLit c α).1 = (φ.bLit c α).2) |
| 81 | |
| 82 | /-- The formula has a satisfying assignment. -/ |
| 83 | def Satisfiable : Prop := ∃ a : φ.Assignment, φ.Satisfies a |
| 84 | |
| 85 | end Formula |
| 86 | |
| 87 | /-- The number of literal positions: two per clause of two literals, three per clause of |
| 88 | three. -/ |
| 89 | def slots (φ : Formula) : ℕ := 2 * φ.twoClauses + 3 * φ.threeClauses |
| 90 | |
| 91 | /-- A formula as a binary word: the number of variables, the numbers of clauses of two and of |
| 92 | three literals, then the variable and sign of each literal of each clause, the clauses of |
| 93 | two literals first. -/ |
| 94 | def encodeFormula (φ : Formula) : Word := |
| 95 | encodeNat φ.vars ++ encodeNat φ.twoClauses ++ encodeNat φ.threeClauses ++ |
| 96 | ((List.finRange φ.twoClauses).flatMap fun c => |
| 97 | (List.finRange 2).flatMap fun α => encodeNat (φ.aLit c α).1 ++ [(φ.aLit c α).2]) ++ |
| 98 | (List.finRange φ.threeClauses).flatMap fun c => |
| 99 | (List.finRange 3).flatMap fun α => encodeNat (φ.bLit c α).1 ++ [(φ.bLit c α).2] |
| 100 | |
| 101 | /-- **[2,3]-bounded 3-SAT** as a language: the encodings of satisfiable formulas with at |
| 102 | most as many variables as literal positions. -/ |
| 103 | def SAT23 : Language := |
| 104 | {w | ∃ φ : Formula, encodeFormula φ = w ∧ φ.vars ≤ slots φ ∧ φ.Satisfiable} |
| 105 | |
| 106 | /-- **[2,3]-bounded 3-SAT is NP-hard.** Every language in NP has a polynomial-time |
| 107 | many-one reduction to it. -/ |
| 108 | axiom npHard : |
| 109 | ∀ A : Language, A ∈ NP → Lax429075.Reductions.ManyOne A SAT23 |
| 110 | |
| 111 | end Lax345332.TwoThreeSat |
| 112 |
Formalization Notes
The definitions are those of the FairRIS submission, copied so that the two problems are literally the same: clauses of two literals and clauses of three literals are separate families, because the constructions that consume such a formula treat them differently.
A formula is written as a binary word in the self-delimiting code of the scheduling submissions: a number is its binary digits preceded by their count in unary. This is not the unary code of the Cook–Levin submission that uses, and the theorem is stated for the words the scheduling submissions read.
The language only contains formulas with at most as many variables as literal positions. This excludes nothing from a formula in which every variable occurs. It is needed because the number of variables is written in binary: a word could name exponentially many variables without using them, and a reduction that writes something for each one could not run in polynomial time.
The occurrence bound is part of the formula, as a proof that each literal occupies at most two of the positions inside the clauses.
Builds on
Used by
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments