(3,4)-Satisfiability
Lax888481.SatVariant · concepts/Lax888481/SatVariant.lean · lax-888481
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.
In the paper
- page 4 of this submission's paper
Lean source view on GitHub
| 1 | import Lax429075.Reductions |
| 2 | import Lax429075.Satisfiability |
| 3 | import Lax888481.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 proved in the submission `lax-345332`, from which the proofs |
| 23 | of this submission take it: the language of that submission is this one. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax888481.SatVariant |
| 27 | |
| 28 | open Lax429075.CNF Lax434930.PolynomialTime |
| 29 | |
| 30 | /-- The number of occurrences of the variable `i` in the formula `F`. -/ |
| 31 | def occurrences (F : Formula) (i : ℕ) : ℕ := |
| 32 | (F.flatMap fun C => C.filter fun l => l.index == i).length |
| 33 | |
| 34 | /-- The variables occurring in `F`. -/ |
| 35 | def occurringVars (F : Formula) : List ℕ := (F.flatMap id).map Literal.index |
| 36 | |
| 37 | /-- `F` is a *(3,4)* formula: every clause has exactly three literals, and every variable |
| 38 | occurs at most four times. -/ |
| 39 | def Exact34 (F : Formula) : Prop := |
| 40 | (∀ C ∈ F, C.length = 3) ∧ ∀ i ∈ occurringVars F, occurrences F i ≤ 4 |
| 41 | |
| 42 | /-- **(3,4)-SAT** as a language: the encodings of satisfiable (3,4) |
| 43 | formulas. -/ |
| 44 | def SAT34 : Language := |
| 45 | {w | ∃ F : Formula, Lax429075.Encoding.encodeCNF F = w ∧ Exact34 F ∧ Satisfiable F} |
| 46 | |
| 47 | /-- **Tovey's theorem.** (3,4)-SAT is NP-hard. |
| 48 | |
| 49 | Tovey, *A simplified NP-complete satisfiability problem*, Discrete Applied Mathematics 8 |
| 50 | (1984) 85–89. -/ |
| 51 | axiom sat34_npHard : |
| 52 | ∀ A : Language, A ∈ Lax434930.NondeterministicPolynomialTime.NP → |
| 53 | Lax429075.Reductions.ManyOne A SAT34 |
| 54 | |
| 55 | end Lax888481.SatVariant |
| 56 |
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 proved in the submission , from which the proofs of this submission take it: the language of that submission is this one.
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