Documentation

DescriptiveComplexity.Problems.OneInSat.Slots

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 :

The three slots of a clause.

one : Ix3
The first occurrence.
two : Ix3
The second occurrence.
three : Ix3
The third occurrence.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instDecidableEqIx3 :

DecidableEq Ix3

Equations

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

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instFintypeIx3 :

Equations

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

Dependency graph

instance DescriptiveComplexity.OneInRed.instNonemptyIx3 :

Dependency graph

inductive DescriptiveComplexity.OneInRed.Ix4 :

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.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instDecidableEqIx4 :

DecidableEq Ix4

Equations

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

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.OneInRed.instFintypeIx4 :

Equations

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

Dependency graph

instance DescriptiveComplexity.OneInRed.instNonemptyIx4 :

Dependency graph

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✝

Instances For

Dependency graph

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.

Dependency graph

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

Dependency graph

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.

Dependency graph

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.

Dependency graph

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) :

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

Instances For

Dependency graph

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

Dependency graph

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.

Dependency graph

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✝

Instances For

Dependency graph

@[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

Dependency graph