3-dimensional matching
Lax799700.ThreeDimMatching · concepts/Lax799700/ThreeDimMatching.lean · lax-799700
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
3-DIMENSIONAL MATCHING: given three marked classes and a set of triples, one element from each class, is there a set of triples covering every marked element exactly once? The vocabulary carries three unary marks and one ternary relation, and a yes-instance admits a matching (IsMatchingOn), a sub-relation of the triples that covers each marked element exactly once; nothing asks the three classes to be disjoint or to exhaust the universe. Membership is by an existential second-order definition, hardness by an ordered first-order reduction from SAT.
Concept map
Evidence
This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.
1 hasThreeDimMatching_iso proven
2 threeDimMatching_iff proven
3 threeDimMatching_NP_complete proven
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Mathlib.ModelTheory.Complexity |
| 3 | import Mathlib.Tactic.FinCases |
| 4 | import Mathlib.ModelTheory.Syntax |
| 5 | import Lax904597.Classes |
| 6 | import Lax799700.Problems |
| 7 | |
| 8 | /-! |
| 9 | --- |
| 10 | title: 3-dimensional matching |
| 11 | type: theorem |
| 12 | --- |
| 13 | 3-DIMENSIONAL MATCHING: given three marked classes and a set of triples, |
| 14 | one element from each class, is there a set of triples covering every |
| 15 | marked element exactly once? The vocabulary carries three unary marks and |
| 16 | one ternary relation, and a yes-instance admits a matching |
| 17 | (IsMatchingOn), a sub-relation of the triples that covers each marked |
| 18 | element exactly once; nothing asks the three classes to be disjoint or |
| 19 | to exhaust the universe. Membership is by an existential second-order |
| 20 | definition, hardness by an ordered first-order reduction from SAT. |
| 21 | |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax799700.ThreeDimMatching |
| 25 | |
| 26 | open FirstOrder |
| 27 | |
| 28 | open FirstOrder.Language |
| 29 | |
| 30 | /-- The relation symbols of the language. -/ |
| 31 | inductive tripleSysRel : ℕ → Type where |
| 32 | /-- `xEl a`: `a` belongs to the first class. -/ |
| 33 | | xEl : tripleSysRel 1 |
| 34 | /-- `yEl a`: `a` belongs to the second class. -/ |
| 35 | | yEl : tripleSysRel 1 |
| 36 | /-- `zEl a`: `a` belongs to the third class. -/ |
| 37 | | zEl : tripleSysRel 1 |
| 38 | /-- `trip a b c`: `(a, b, c)` is one of the available triples. -/ |
| 39 | | trip : tripleSysRel 3 |
| 40 | deriving DecidableEq |
| 41 | |
| 42 | /-- The relational language of triple systems: three marked classes and a |
| 43 | ternary relation. -/ |
| 44 | def tripleSys : FirstOrder.Language := |
| 45 | ⟨fun _ => Empty, tripleSysRel⟩ |
| 46 | |
| 47 | instance instIsRelationalTripleSys : FirstOrder.Language.IsRelational tripleSys := fun _ => |
| 48 | (inferInstance : IsEmpty Empty) |
| 49 | |
| 50 | /-- `xEl a`: `a` belongs to the first class. -/ |
| 51 | abbrev tsXEl : tripleSys.Relations 1 := |
| 52 | .xEl |
| 53 | |
| 54 | /-- `yEl a`: `a` belongs to the second class. -/ |
| 55 | abbrev tsYEl : tripleSys.Relations 1 := |
| 56 | .yEl |
| 57 | |
| 58 | /-- `zEl a`: `a` belongs to the third class. -/ |
| 59 | abbrev tsZEl : tripleSys.Relations 1 := |
| 60 | .zEl |
| 61 | |
| 62 | /-- `trip a b c`: `(a, b, c)` is one of the available triples. -/ |
| 63 | abbrev tsTrip : tripleSys.Relations 3 := |
| 64 | .trip |
| 65 | |
| 66 | open FirstOrder |
| 67 | |
| 68 | open Language Structure |
| 69 | |
| 70 | section Shorthands |
| 71 | |
| 72 | variable {A : Type} [tripleSys.Structure A] |
| 73 | |
| 74 | /-- `xEl a`: `a` belongs to the first class. -/ |
| 75 | def TSXEl {A : Type} [tripleSys.Structure A] (a0 : A) : Prop := |
| 76 | FirstOrder.Language.Structure.RelMap tsXEl ![a0] |
| 77 | |
| 78 | /-- `yEl a`: `a` belongs to the second class. -/ |
| 79 | def TSYEl {A : Type} [tripleSys.Structure A] (a0 : A) : Prop := |
| 80 | FirstOrder.Language.Structure.RelMap tsYEl ![a0] |
| 81 | |
| 82 | /-- `zEl a`: `a` belongs to the third class. -/ |
| 83 | def TSZEl {A : Type} [tripleSys.Structure A] (a0 : A) : Prop := |
| 84 | FirstOrder.Language.Structure.RelMap tsZEl ![a0] |
| 85 | |
| 86 | /-- `trip a b c`: `(a, b, c)` is one of the available triples. -/ |
| 87 | def TSTrip {A : Type} [tripleSys.Structure A] (a0 : A) (a1 : A) (a2 : A) : Prop := |
| 88 | FirstOrder.Language.Structure.RelMap tsTrip ![a0, a1, a2] |
| 89 | |
| 90 | end Shorthands |
| 91 | |
| 92 | section Matching |
| 93 | |
| 94 | variable {A : Type} |
| 95 | |
| 96 | /-- A **matching**: a set of triples, taken from `T` and lying in the three |
| 97 | classes, covering every marked element exactly once. -/ |
| 98 | def IsMatchingOn (X Y Z : A → Prop) (T : A → A → A → Prop) (M : A → A → A → Prop) : Prop := |
| 99 | (∀ x y z, M x y z → T x y z ∧ X x ∧ Y y ∧ Z z) ∧ |
| 100 | (∀ x, X x → ∃ y z, M x y z) ∧ (∀ y, Y y → ∃ x z, M x y z) ∧ |
| 101 | (∀ z, Z z → ∃ x y, M x y z) ∧ |
| 102 | (∀ x y z y' z', M x y z → M x y' z' → y = y' ∧ z = z') ∧ |
| 103 | (∀ x y z x' z', M x y z → M x' y z' → x = x' ∧ z = z') ∧ |
| 104 | ∀ x y z x' y', M x y z → M x' y' z → x = x' ∧ y = y' |
| 105 | |
| 106 | end Matching |
| 107 | |
| 108 | section Problem |
| 109 | |
| 110 | variable (A : Type) [tripleSys.Structure A] |
| 111 | |
| 112 | /-- A triple system is a yes-instance when some subset of its triples covers |
| 113 | each marked element exactly once. -/ |
| 114 | def HasThreeDimMatching : Prop := |
| 115 | Finite A ∧ ∃ M : A → A → A → Prop, |
| 116 | IsMatchingOn (TSXEl (A := A)) TSYEl TSZEl TSTrip M |
| 117 | |
| 118 | end Problem |
| 119 | |
| 120 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems |
| 121 | |
| 122 | /-- The property `HasThreeDimMatching` is isomorphism-invariant. -/ |
| 123 | axiom hasThreeDimMatching_iso : ∀ {A B : Type} [Lax799700.ThreeDimMatching.tripleSys.Structure A] [Lax799700.ThreeDimMatching.tripleSys.Structure B], |
| 124 | (A ≃[Lax799700.ThreeDimMatching.tripleSys] B) → (HasThreeDimMatching A ↔ HasThreeDimMatching B) |
| 125 | |
| 126 | /-- The problem ThreeDimMatching: does the structure satisfy `HasThreeDimMatching`? -/ |
| 127 | def ThreeDimMatching : DecisionProblem Lax799700.ThreeDimMatching.tripleSys := |
| 128 | DecisionProblem.ofPred HasThreeDimMatching |
| 129 | |
| 130 | /-- The yes-instances of ThreeDimMatching are exactly the structures |
| 131 | satisfying `HasThreeDimMatching`. -/ |
| 132 | axiom threeDimMatching_iff : ∀ (A : Type) [Lax799700.ThreeDimMatching.tripleSys.Structure A], ThreeDimMatching A ↔ HasThreeDimMatching A |
| 133 | |
| 134 | /-- ThreeDimMatching is NP-complete. -/ |
| 135 | axiom threeDimMatching_NP_complete : NP.Complete ThreeDimMatching |
| 136 | |
| 137 | end Lax799700.ThreeDimMatching |
| 138 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments