The three slots of a clause

The semantic layer of the reduction of 3SAT to 1-in-SAT. Under the width bound, a clause has at most three occurrences, so naming them first, second and third – DescriptiveComplexity.OneInRed.NthOcc, defined by walking the occurrence order from the minimum – covers all of them (DescriptiveComplexity.OneInRed.exists_nthOcc). The gadget then works with three slots per clause, whether or not the corresponding occurrence exists, which is what removes the width case analysis from the classical construction.

The formulas defining NthOcc over the ordered expansion, and their realization lemmas, are here too: they are built from minOccF and succOccF of DescriptiveComplexity.OccurrenceFormulas.

inductive DescriptiveComplexity.OneInRed.Ix3 : Type

The three slots of a clause.

• one : Ix3

  The first occurrence.

• two : Ix3

  The second occurrence.

• three : Ix3

  The third occurrence.

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instDecidableEqIx3 : DecidableEq Ix3

Equations

• DescriptiveComplexity.OneInRed.instDecidableEqIx3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instFintypeIx3 : Fintype Ix3

Equations

• One or more equations did not get rendered due to their size.

instance DescriptiveComplexity.OneInRed.instNonemptyIx3 : Nonempty Ix3

inductive DescriptiveComplexity.OneInRed.Ix4 : Type

The four fresh variables of the gadget of a clause.

• d : Ix4

  d, of the first gadget clause.

• e : Ix4

  e, shared by the first two gadget clauses.

• f : Ix4

  f, shared by the last two gadget clauses.

• g : Ix4

  g, of the last gadget clause.

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instDecidableEqIx4 : DecidableEq Ix4

Equations

• DescriptiveComplexity.OneInRed.instDecidableEqIx4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instFintypeIx4 : Fintype Ix4

Equations

• One or more equations did not get rendered due to their size.

instance DescriptiveComplexity.OneInRed.instNonemptyIx4 : Nonempty Ix4

The i-th occurrence of a clause

def DescriptiveComplexity.OneInRed.NthOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : Ix3 → A → A → Bool → Prop

(x, s) is the i-th occurrence of c, counted from the first one along the occurrence order.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.OneInRed.NthOcc DescriptiveComplexity.OneInRed.Ix3.one x✝² x✝¹ x✝ = DescriptiveComplexity.SatOcc.MinOcc x✝² x✝¹ x✝

theorem DescriptiveComplexity.OneInRed.minOcc_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x y : A} {s t : Bool} (h₁ : SatOcc.MinOcc c x s) (h₂ : SatOcc.MinOcc c y t) : x = y ∧ s = t

The first occurrence of a clause is unique.

theorem DescriptiveComplexity.OneInRed.NthOcc.occIn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {i : Ix3} {c x : A} {s : Bool} (h : NthOcc i c x s) : SatOcc.OccIn c x s

theorem DescriptiveComplexity.OneInRed.nthOcc_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {i : Ix3} {c x y : A} {s t : Bool} (h₁ : NthOcc i c x s) (h₂ : NthOcc i c y t) : x = y ∧ s = t

The i-th occurrence of a clause is unique.

theorem DescriptiveComplexity.OneInRed.exists_nthOcc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hw : WidthAtMostThree A) {c x : A} {s : Bool} (h : SatOcc.OccIn c x s) : ∃ (i : Ix3), NthOcc i c x s

Under the width bound every occurrence is one of the first three. A fourth one would exhibit a chain of four distinct occurrences of the same clause.

The value carried by a slot

def DescriptiveComplexity.OneInRed.SlotVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (i : Ix3) (c : A) : Prop

The value of the i-th slot of c under ν: the value of the i-th literal of c, and False when c has no i-th occurrence.

Equations

• DescriptiveComplexity.OneInRed.SlotVal ν i c = ∃ (x : A) (s : Bool), DescriptiveComplexity.OneInRed.NthOcc i c x s ∧ DescriptiveComplexity.SatOcc.LitTrue ν x s

theorem DescriptiveComplexity.OneInRed.slotVal_of_nth {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {i : Ix3} {c x : A} {s : Bool} (h : NthOcc i c x s) : SlotVal ν i c ↔ SatOcc.LitTrue ν x s

theorem DescriptiveComplexity.OneInRed.exists_litTrue_iff_slot {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] (hw : WidthAtMostThree A) {ν : A → Prop} {c : A} : (∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) ↔ SlotVal ν Ix3.one c ∨ SlotVal ν Ix3.two c ∨ SlotVal ν Ix3.three c

A clause has a true literal iff one of its three slots is true.

The i-th occurrence, as a formula

noncomputable def DescriptiveComplexity.OneInRed.nthF {α : Type} : Ix3 → Bool → α → α → SatOcc.satOrd.Formula α

(x, s) is the i-th occurrence of c, as a formula.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.OneInRed.nthF DescriptiveComplexity.OneInRed.Ix3.one x✝² x✝¹ x✝ = DescriptiveComplexity.SatOcc.minOccF x✝² x✝¹ x✝

@[simp]

theorem DescriptiveComplexity.OneInRed.realize_nthF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {i : Ix3} {s : Bool} {c x : α} : (nthF i s c x).Realize v ↔ NthOcc i (v c) (v x) s

Home · Documentation · Publications · Contributors · Source · Cite