(3,4)-satisfiability
Lax470956.SatVariant · concepts/Lax470956/SatVariant.lean · lax-470956
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
(3,4)-SAT is satisfiability restricted to formulas in which every clause contains exactly three literals and every variable occurs at most four times. Tovey proved that it is NP-hard; it is the starting point of the second theorem of this submission, because the bounded number of occurrences is what keeps the processing times of the scheduling instance the reduction builds bounded by an absolute constant.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
No proof in the archive yet — this claim is open.
Lean source view on GitHub
| 1 | import Lax429075.Reductions |
| 2 | import Lax429075.Satisfiability |
| 3 | import Lax470956.NPHardness |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: (3,4)-satisfiability |
| 8 | type: definition |
| 9 | --- |
| 10 | *(3,4)-SAT* is satisfiability restricted to formulas in which every clause contains |
| 11 | exactly three literals and every variable occurs at most four times. Tovey proved |
| 12 | that it is NP-hard; it is the starting point of the second theorem of this submission, |
| 13 | because the bounded number of occurrences is what keeps the processing times of the |
| 14 | scheduling instance the reduction builds bounded by an absolute constant. |
| 15 | |
| 16 | # Formalization notes |
| 17 | |
| 18 | The restriction is a predicate on the CNF formulas of the archive's Cook–Levin submission, |
| 19 | so the encoding and the notion of satisfiability are shared with unrestricted SAT. |
| 20 | Occurrences are counted with multiplicity. |
| 21 | |
| 22 | Tovey's theorem is stated here and not proved; Theorem 2 assumes it. |
| 23 | -/ |
| 24 | |
| 25 | namespace Lax470956.SatVariant |
| 26 | |
| 27 | open Lax429075.CNF Lax434930.PolynomialTime |
| 28 | |
| 29 | /-- The number of occurrences of the variable `i` in the formula `F`. -/ |
| 30 | def occurrences (F : Formula) (i : ℕ) : ℕ := |
| 31 | (F.flatMap fun C => C.filter fun l => l.index == i).length |
| 32 | |
| 33 | /-- The variables occurring in `F`. -/ |
| 34 | def occurringVars (F : Formula) : List ℕ := (F.flatMap id).map Literal.index |
| 35 | |
| 36 | /-- `F` is a *(3,4)* formula: every clause has exactly three literals, and every variable |
| 37 | occurs at most four times. -/ |
| 38 | def Exact34 (F : Formula) : Prop := |
| 39 | (∀ C ∈ F, C.length = 3) ∧ ∀ i ∈ occurringVars F, occurrences F i ≤ 4 |
| 40 | |
| 41 | /-- **(3,4)-SAT** as a language: the encodings of satisfiable (3,4) |
| 42 | formulas. -/ |
| 43 | def SAT34 : Language := |
| 44 | {w | ∃ F : Formula, Lax429075.Encoding.encodeCNF F = w ∧ Exact34 F ∧ Satisfiable F} |
| 45 | |
| 46 | /-- **Tovey's theorem.** (3,4)-SAT is NP-hard. |
| 47 | |
| 48 | Tovey, *A simplified NP-complete satisfiability problem*, Discrete Applied Mathematics 8 |
| 49 | (1984) 85–89. -/ |
| 50 | axiom sat34_npHard : |
| 51 | ∀ A : Language, A ∈ Lax434930.NondeterministicPolynomialTime.NP → |
| 52 | Lax429075.Reductions.ManyOne A SAT34 |
| 53 | |
| 54 | end Lax470956.SatVariant |
| 55 |
Formalization notes
The restriction is a predicate on the CNF formulas of the archive's Cook–Levin submission, so the encoding and the notion of satisfiability are shared with unrestricted SAT. Occurrences are counted with multiplicity.
Tovey's theorem is stated here and not proved; Theorem 2 assumes it.
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments