Documentation

DescriptiveComplexity.Problems.Qsat.Matrix

The matrix of the constructed instance #

What the matrix of the QSAT instance built by the Savitch reduction says, clause tag by clause tag.

A clause is satisfied when one of the literals of its list (DescriptiveComplexity.qLits) is (DescriptiveComplexity.ClSat), and a literal is satisfied when the variable its link points at gets the literal's sign (DescriptiveComplexity.LitSat). Since every link pins the coordinates of that variable, the existential quantifier of a literal collapses (DescriptiveComplexity.litSat_atP and its companions, one per DescriptiveComplexity.QLink), and each clause tag turns into a plain condition on what the valuation reads (DescriptiveComplexity.clSat_cSrc and its companions).

def DescriptiveComplexity.LitSat {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (σ : QM A → Prop) (p q : A) (l : QLit) :

A literal of a clause sitting at (p, q) is satisfied by the valuation σ: the variable its link points at gets its sign.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.ClSat {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (σ : QM A → Prop) (c : QClTag) (p q : A) :

A clause of the constructed instance is satisfied by the valuation σ.

Equations

DescriptiveComplexity.ClSat σ c p q = ∃ l ∈ DescriptiveComplexity.qLits c, DescriptiveComplexity.LitSat σ p q l

Instances For

Dependency graph

theorem DescriptiveComplexity.qsatMatrix_iff {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] (σ : QM A → Prop) :

QsatMatrix σ ↔ ∀ (c : QClTag) (p q : A), QClOn c p q → ClSat σ c p q

The matrix of the constructed instance: every guarded clause tag is satisfied.

Dependency graph

Collapsing the quantifier of a literal #

Every link pins the coordinates of the variable it points at, except the two that range over the literals of a clause of the input.

@[simp]

theorem DescriptiveComplexity.litSat_atP {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.atP } ↔ QVarOn vt p (qBot A) ∧ (σ (qVar vt p (qBot A)) ↔ sgn = true)

Dependency graph

@[simp]

theorem DescriptiveComplexity.litSat_atQ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.atQ } ↔ QVarOn vt q (qBot A) ∧ (σ (qVar vt q (qBot A)) ↔ sgn = true)

Dependency graph

@[simp]

theorem DescriptiveComplexity.litSat_botBoth {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.botBoth } ↔ QVarOn vt (qBot A) (qBot A) ∧ (σ (qVar vt (qBot A) (qBot A)) ↔ sgn = true)

Dependency graph

@[simp]

theorem DescriptiveComplexity.litSat_same {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.same } ↔ QVarOn vt p q ∧ (σ (qVar vt p q) ↔ sgn = true)

Dependency graph

@[simp]

theorem DescriptiveComplexity.litSat_maxAtP {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.maxAtP } ↔ ∃ (m : A), IsMaxSV m ∧ QVarOn vt m p ∧ (σ (qVar vt m p) ↔ sgn = true)

Dependency graph

@[simp]

theorem DescriptiveComplexity.litSat_minAtQ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.minAtQ } ↔ IsMinSV p ∧ QVarOn vt q (qBot A) ∧ (σ (qVar vt q (qBot A)) ↔ sgn = true)

Dependency graph

@[simp]

theorem DescriptiveComplexity.litSat_predAtQ {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.predAtQ } ↔ ∃ (d : A), IsPredSV d p ∧ QVarOn vt d q ∧ (σ (qVar vt d q) ↔ sgn = true)

Dependency graph

@[simp]

theorem DescriptiveComplexity.litSat_occPos {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.occPos } ↔ ∃ (r : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![p, r] ∧ QVarOn vt r (qBot A) ∧ (σ (qVar vt r (qBot A)) ↔ sgn = true)

Dependency graph

@[simp]

theorem DescriptiveComplexity.litSat_occNeg {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {σ : QM A → Prop} {p q : A} {vt : QVarTag} {sgn : Bool} :

LitSat σ p q { vt := vt, sign := sgn, link := QLink.occNeg } ↔ ∃ (r : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![p, r] ∧ QVarOn vt r (qBot A) ∧ (σ (qVar vt r (qBot A)) ↔ sgn = true)

Dependency graph

What each clause says #

@[simp]

theorem DescriptiveComplexity.and_isSV_of_isMaxSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {m : A} {P : Prop} :

IsMaxSV m ∧ IsSV m ∧ P ↔ IsMaxSV m ∧ P

Dependency graph

@[simp]

theorem DescriptiveComplexity.and_isSV_of_isPredSV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] {d ℓ : A} {P : Prop} :

IsPredSV d ℓ ∧ IsSV d ∧ P ↔ IsPredSV d ℓ ∧ P

Dependency graph

theorem DescriptiveComplexity.clSat_cSrc {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (p q : A) :

ClSat σ QClTag.cSrc p q ↔ ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![p, x] ∧ valS σ x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![p, x] ∧ ¬valS σ x

A copy of a source clause reads its literals on the source valuation.

Dependency graph

theorem DescriptiveComplexity.clSat_cTgt {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (p q : A) :

ClSat σ QClTag.cTgt p q ↔ ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![p, x] ∧ valT σ x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![p, x] ∧ ¬valT σ x

A copy of a target clause reads its literals on the target valuation.

Dependency graph

theorem DescriptiveComplexity.clSat_cStep {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (p q : A) :

ClSat σ QClTag.cStep p q ↔ bitE σ ∨ ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsPosIn ![p, x] ∧ valP σ x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.tsNegIn ![p, x] ∧ ¬valP σ x

A copy of a transition clause reads its literals on the transition valuation, unless the base case is the equality branch.

Dependency graph

theorem DescriptiveComplexity.clSat_lS {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (s : Bool) {p q : A} (hg : QClOn (QClTag.lS s) p q) :

ClSat σ (QClTag.lS s) p q ↔ (valS σ p ↔ s = true) ∨ (stS σ p ↔ (!s) = true)

The source valuation reads the source endpoint.

Dependency graph

theorem DescriptiveComplexity.clSat_lT {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (s : Bool) {p q : A} (hg : QClOn (QClTag.lT s) p q) :

ClSat σ (QClTag.lT s) p q ↔ (valT σ p ↔ s = true) ∨ (stT σ p ↔ (!s) = true)

The target valuation reads the target endpoint.

Dependency graph

theorem DescriptiveComplexity.clSat_lU {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (s : Bool) {p q : A} (hg : QClOn (QClTag.lU s) p q) :

ClSat σ (QClTag.lU s) p q ↔ bitE σ ∨ (valP σ p ↔ s = true) ∨ ∃ (m : A), IsMaxSV m ∧ (stU σ m p ↔ (!s) = true)

The transition valuation reads the first component of the bottom pair.

Dependency graph

theorem DescriptiveComplexity.clSat_lV {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (s : Bool) {p q : A} (hg : QClOn (QClTag.lV s) p q) :

ClSat σ (QClTag.lV s) p q ↔ bitE σ ∨ (valP σ q ↔ s = true) ∨ ∃ (m : A), IsMaxSV m ∧ (stV σ m p ↔ (!s) = true)

The transition valuation writes the second component of the bottom pair.

Dependency graph

theorem DescriptiveComplexity.clSat_bE {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (s : Bool) {p q : A} (hg : QClOn (QClTag.bE s) p q) :

ClSat σ (QClTag.bE s) p q ↔ ¬bitE σ ∨ (∃ (m : A), IsMaxSV m ∧ (stU σ m p ↔ s = true)) ∨ ∃ (m : A), IsMaxSV m ∧ (stV σ m p ↔ (!s) = true)

The equality branch of the base case.

Dependency graph

def DescriptiveComplexity.LevSat {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (b w s : Bool) (ℓ x : A) :

What one of the eight clauses of a level says: the branch of the universal bit, the component of the pair it constrains, and the value that component must copy – the midpoint, or the endpoint the level receives from above.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.clSat_lev {A : Type} [FirstOrder.Language.transSys.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (σ : QM A → Prop) (b w s : Bool) {ℓ x : A} (hg : QClOn (QClTag.lev b w s) ℓ x) :

ClSat σ (QClTag.lev b w s) ℓ x ↔ LevSat σ b w s ℓ x

A level clause says exactly what DescriptiveComplexity.LevSat says.

Dependency graph