Satisfiability of Bounded Occurrence
Lax117284.BoundedSat · concepts/Lax117284/BoundedSat.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A [2,3]-bounded 3-SAT formula is a conjunction of clauses of two and of three literals in which every literal occurs at most twice — so every variable occurs at most twice positively and at most twice negatively, and hence in at most four clauses. Deciding whether such a formula is satisfiable is NP-hard.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax117284.Problems |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Satisfiability of Bounded Occurrence |
| 6 | type: definition |
| 7 | --- |
| 8 | A *[2,3]-bounded 3-SAT formula* is a conjunction of clauses of two and of three literals in |
| 9 | which every literal occurs at most twice — so every variable occurs at most twice |
| 10 | positively and at most twice negatively, and hence in at most four clauses. Deciding |
| 11 | whether such a formula is satisfiable is NP-hard. |
| 12 | |
| 13 | # Formalization Notes |
| 14 | |
| 15 | The two widths are separate families of clauses rather than one family with a width |
| 16 | condition, because the construction that consumes such a formula treats the two widths |
| 17 | differently: the clauses of three literals receive a gadget of their own. |
| 18 | |
| 19 | The language contains only formulas with at most as many variables as positions. A formula |
| 20 | in which every variable occurs is of this kind, so nothing is excluded that a formula of the |
| 21 | paper is; but the number of variables is written in binary, so a word may name exponentially |
| 22 | many variables without mentioning any, and a reduction that writes a client for each of them |
| 23 | could not run in polynomial time. |
| 24 | |
| 25 | The occurrence bound is a condition on the formula and not extra data: an *occurrence* is a |
| 26 | position inside a clause, and every literal is required to occupy at most two of them. A |
| 27 | reduction that needs to distinguish the two occurrences of a literal obtains a numbering of |
| 28 | them from this bound. |
| 29 | -/ |
| 30 | |
| 31 | namespace Lax117284.BoundedSat |
| 32 | |
| 33 | open Lax434930.PolynomialTime Lax434930.NondeterministicPolynomialTime |
| 34 | |
| 35 | /-- A **[2,3]-bounded 3-SAT formula** over `vars` variables: `twoClauses` clauses of two |
| 36 | literals and `threeClauses` clauses of three literals, in which every literal — a variable |
| 37 | together with a sign — occupies at most two of the positions of the formula. -/ |
| 38 | structure Formula where |
| 39 | /-- The number of variables. -/ |
| 40 | vars : ℕ |
| 41 | /-- The number of clauses of two literals. -/ |
| 42 | twoClauses : ℕ |
| 43 | /-- The number of clauses of three literals. -/ |
| 44 | threeClauses : ℕ |
| 45 | /-- The literals of the clauses of two literals. -/ |
| 46 | aLit : Fin twoClauses → Fin 2 → Fin vars × Bool |
| 47 | /-- The literals of the clauses of three literals. -/ |
| 48 | bLit : Fin threeClauses → Fin 3 → Fin vars × Bool |
| 49 | /-- Every literal occurs at most twice in the formula. -/ |
| 50 | occ_le_two : ∀ l : Fin vars × Bool, |
| 51 | (Finset.univ.filter fun o : (Fin twoClauses × Fin 2) ⊕ (Fin threeClauses × Fin 3) => |
| 52 | Sum.elim (fun q => aLit q.1 q.2) (fun q => bLit q.1 q.2) o = l).card ≤ 2 |
| 53 | |
| 54 | namespace Formula |
| 55 | |
| 56 | variable (φ : Formula) |
| 57 | |
| 58 | /-- A **position** of the formula: a literal slot in one of the clauses. -/ |
| 59 | abbrev Occ := (Fin φ.twoClauses × Fin 2) ⊕ (Fin φ.threeClauses × Fin 3) |
| 60 | |
| 61 | /-- The literal occupying a position. -/ |
| 62 | def litAt (o : φ.Occ) : Fin φ.vars × Bool := |
| 63 | Sum.elim (fun q => φ.aLit q.1 q.2) (fun q => φ.bLit q.1 q.2) o |
| 64 | |
| 65 | /-- An assignment of a truth value to every variable. -/ |
| 66 | abbrev Assignment := Fin φ.vars → Bool |
| 67 | |
| 68 | /-- The assignment `a` satisfies `φ`: every clause, of either width, has a literal that |
| 69 | holds. -/ |
| 70 | def Satisfies (a : φ.Assignment) : Prop := |
| 71 | (∀ c, ∃ α, a (φ.aLit c α).1 = (φ.aLit c α).2) ∧ |
| 72 | (∀ c, ∃ α, a (φ.bLit c α).1 = (φ.bLit c α).2) |
| 73 | |
| 74 | /-- **The question of [2,3]-bounded 3-SAT**: is there a satisfying assignment? -/ |
| 75 | def Satisfiable : Prop := ∃ a : φ.Assignment, φ.Satisfies a |
| 76 | |
| 77 | end Formula |
| 78 | |
| 79 | /-- The literal occupying the occurrence slot `o`, read off unnumbered indices: the two |
| 80 | slots of every clause of two literals come first, then the three slots of every clause of |
| 81 | three literals. Outside the formula the value is the positive literal of the variable `0`. |
| 82 | It is in this form that a construction reads a formula. -/ |
| 83 | def litOfSlot (φ : Formula) (o : ℕ) : ℕ × Bool := |
| 84 | if o < 2 * φ.twoClauses then |
| 85 | if hj : o / 2 < φ.twoClauses then |
| 86 | ((φ.aLit ⟨o / 2, hj⟩ ⟨o % 2, by omega⟩).1, (φ.aLit ⟨o / 2, hj⟩ ⟨o % 2, by omega⟩).2) |
| 87 | else (0, true) |
| 88 | else |
| 89 | if hj : (o - 2 * φ.twoClauses) / 3 < φ.threeClauses then |
| 90 | ((φ.bLit ⟨(o - 2 * φ.twoClauses) / 3, hj⟩ ⟨(o - 2 * φ.twoClauses) % 3, by omega⟩).1, |
| 91 | (φ.bLit ⟨(o - 2 * φ.twoClauses) / 3, hj⟩ ⟨(o - 2 * φ.twoClauses) % 3, by omega⟩).2) |
| 92 | else (0, true) |
| 93 | |
| 94 | /-- Which of the occurrences of its own literal the slot `o` is: the number of earlier |
| 95 | slots carrying the same literal. Under the occurrence bound this is `0` or `1`. -/ |
| 96 | def slotRank (φ : Formula) (o : ℕ) : ℕ := |
| 97 | (List.range o).countP fun o' => litOfSlot φ o' == litOfSlot φ o |
| 98 | |
| 99 | /-- The number of occurrence slots of the formula. -/ |
| 100 | def slots (φ : Formula) : ℕ := 2 * φ.twoClauses + 3 * φ.threeClauses |
| 101 | |
| 102 | /-- A [2,3]-bounded 3-SAT formula as a binary word: the number of variables, the two |
| 103 | numbers of clauses, and then the variable and the sign of every literal of every clause, |
| 104 | the clauses of two literals first. -/ |
| 105 | def encodeFormula (φ : Formula) : Word := |
| 106 | Problems.encodeNat φ.vars ++ Problems.encodeNat φ.twoClauses ++ |
| 107 | Problems.encodeNat φ.threeClauses ++ |
| 108 | ((List.finRange φ.twoClauses).flatMap fun c => |
| 109 | (List.finRange 2).flatMap fun α => |
| 110 | Problems.encodeNat (φ.aLit c α).1 ++ [(φ.aLit c α).2]) ++ |
| 111 | (List.finRange φ.threeClauses).flatMap fun c => |
| 112 | (List.finRange 3).flatMap fun α => |
| 113 | Problems.encodeNat (φ.bLit c α).1 ++ [(φ.bLit c α).2] |
| 114 | |
| 115 | /-- **[2,3]-bounded 3-SAT**, as a language: the satisfiable formulas that have no more |
| 116 | variables than positions, which every formula in which each variable occurs does. -/ |
| 117 | def BoundedSat : Language := |
| 118 | {w | ∃ φ : Formula, encodeFormula φ = w ∧ φ.vars ≤ slots φ ∧ φ.Satisfiable} |
| 119 | |
| 120 | /-- **[2,3]-bounded 3-SAT is NP-hard.** -/ |
| 121 | axiom boundedSat_npHard : Problems.NPHard BoundedSat |
| 122 | |
| 123 | end Lax117284.BoundedSat |
| 124 |
Formalization Notes
The two widths are separate families of clauses rather than one family with a width condition, because the construction that consumes such a formula treats the two widths differently: the clauses of three literals receive a gadget of their own.
The language contains only formulas with at most as many variables as positions. A formula in which every variable occurs is of this kind, so nothing is excluded that a formula of the paper is; but the number of variables is written in binary, so a word may name exponentially many variables without mentioning any, and a reduction that writes a client for each of them could not run in polynomial time.
The occurrence bound is a condition on the formula and not extra data: an occurrence is a position inside a clause, and every literal is required to occupy at most two of them. A reduction that needs to distinguish the two occurrences of a literal obtains a numbering of them from this bound.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments