The occurrences of a variable, cyclically ordered

DescriptiveComplexity.OccurrenceOrder walks the occurrences of a clause; this file walks those of a variable – the same signed positions (c, s), read along the other index – and closes the walk into a cycle (DescriptiveComplexity.SatOcc.VarNext): the last occurrence of a variable is followed by its first one.

That cycle is what a truth-setting gadget needs. A gadget laid along a path of occurrences is forced into a single configuration, and forces the variable to one truth value; laid along a cycle it admits exactly two, which is what makes it an assignment. It is used by the reduction to 3-dimensional matching (DescriptiveComplexity.Problems.ThreeDimMatching.Hardness).

Everything here has a first-order counterpart, over the ordered expansion DescriptiveComplexity.SatOcc.satOrd, since the successor is “the next occurrence, or the first one if there is no next”, and both halves are first-order.

The cyclic order on the occurrences of a variable

def DescriptiveComplexity.SatOcc.VarMin {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x c : A) (s : Bool) : Prop

(c, s) is the first occurrence of the variable x.

Equations

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

def DescriptiveComplexity.SatOcc.VarMax {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x c : A) (s : Bool) : Prop

(c, s) is the last occurrence of the variable x.

Equations

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

def DescriptiveComplexity.SatOcc.VarStep {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x c : A) (s : Bool) (c' : A) (t : Bool) : Prop

(c', t) is the occurrence of x immediately after (c, s).

Equations

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

def DescriptiveComplexity.SatOcc.VarNext {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x c : A) (s : Bool) (c' : A) (t : Bool) : Prop

(c', t) follows (c, s) cyclically among the occurrences of x: the next one, or the first one when (c, s) is the last.

Equations

• DescriptiveComplexity.SatOcc.VarNext x c s c' t = (DescriptiveComplexity.SatOcc.VarStep x c s c' t ∨ DescriptiveComplexity.SatOcc.VarMax x c s ∧ DescriptiveComplexity.SatOcc.VarMin x c' t)

theorem DescriptiveComplexity.SatOcc.VarNext.occIn_left {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x c c' : A} {s t : Bool} (h : VarNext x c s c' t) : OccIn c x s

theorem DescriptiveComplexity.SatOcc.VarNext.occIn_right {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {x c c' : A} {s t : Bool} (h : VarNext x c s c' t) : OccIn c' x t

The first-order counterparts

noncomputable def DescriptiveComplexity.SatOcc.varEarlierF {α : Type} (s : Bool) (x c : α) : satOrd.Formula α

Some occurrence of the variable x lies strictly before (c, s), as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.varLaterF {α : Type} (s : Bool) (x c : α) : satOrd.Formula α

Some occurrence of the variable x lies strictly after (c, s), as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.varMinF {α : Type} (s : Bool) (x c : α) : satOrd.Formula α

(c, s) is the first occurrence of the variable x, as a formula.

Equations

• DescriptiveComplexity.SatOcc.varMinF s x c = DescriptiveComplexity.SatOcc.occF s c x ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SatOcc.varEarlierF s x c)

noncomputable def DescriptiveComplexity.SatOcc.varMaxF {α : Type} (s : Bool) (x c : α) : satOrd.Formula α

(c, s) is the last occurrence of the variable x, as a formula.

Equations

• DescriptiveComplexity.SatOcc.varMaxF s x c = DescriptiveComplexity.SatOcc.occF s c x ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SatOcc.varLaterF s x c)

noncomputable def DescriptiveComplexity.SatOcc.varBetweenF {α : Type} (s t : Bool) (x c c' : α) : satOrd.Formula α

Some occurrence of x lies strictly between (c, s) and (c', t), as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.varStepF {α : Type} (s t : Bool) (x c c' : α) : satOrd.Formula α

(c', t) is the occurrence of x immediately after (c, s), as a formula.

Equations

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

noncomputable def DescriptiveComplexity.SatOcc.varNextF {α : Type} (s t : Bool) (x c c' : α) : satOrd.Formula α

(c', t) follows (c, s) cyclically among the occurrences of x, as a formula.

Equations

• DescriptiveComplexity.SatOcc.varNextF s t x c c' = DescriptiveComplexity.SatOcc.varStepF s t x c c' ⊔ DescriptiveComplexity.SatOcc.varMaxF s x c ⊓ DescriptiveComplexity.SatOcc.varMinF t x c'

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varEarlierF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {x c : α} : (varEarlierF s x c).Realize v ↔ ∃ (c' : A) (t : Bool), OccIn c' (v x) t ∧ occLt c' t (v c) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varLaterF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {x c : α} : (varLaterF s x c).Realize v ↔ ∃ (c' : A) (t : Bool), OccIn c' (v x) t ∧ occLt (v c) s c' t

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varMinF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {x c : α} : (varMinF s x c).Realize v ↔ VarMin (v x) (v c) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varMaxF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {x c : α} : (varMaxF s x c).Realize v ↔ VarMax (v x) (v c) s

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varBetweenF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s t : Bool} {x c c' : α} : (varBetweenF s t x c c').Realize v ↔ ∃ (c'' : A) (u : Bool), OccIn c'' (v x) u ∧ occLt (v c) s c'' u ∧ occLt c'' u (v c') t

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varStepF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s t : Bool} {x c c' : α} : (varStepF s t x c c').Realize v ↔ VarStep (v x) (v c) s (v c') t

@[simp]

theorem DescriptiveComplexity.SatOcc.realize_varNextF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s t : Bool} {x c c' : α} : (varNextF s t x c c').Realize v ↔ VarNext (v x) (v c) s (v c') t