Prefix valuations: the chain of a clause, with determined links

Splitting a wide clause ℓ₁ ∨ ⋯ ∨ ℓₖ into clauses of bounded width threads fresh variables along the linear order of its literal occurrences (DescriptiveComplexity.OccurrenceOrder). The plain chain of the decision reduction leaves those variables free whenever the clause is satisfied early, which a reduction that must preserve the number of solutions cannot afford.

This file isolates the determined variant, independently of any interpretation. A prefix valuation (DescriptiveComplexity.SatOcc.PrefixVal) gives each occurrence (x, s) of each clause c a truth value Z c x s such that

• Z c x s holds iff the literal (x, s) is true or Z holds at the immediately preceding occurrence – three clauses of width at most three;
• Z holds at the last occurrence of every clause – a unit clause;
• there is no empty clause.

Such a Z is then forced to be the truth of the prefix disjunction (DescriptiveComplexity.SatOcc.PrefixVal.iff_prefixOr), so it carries no information beyond the assignment; an assignment has a prefix valuation exactly when it satisfies every clause (DescriptiveComplexity.SatOcc.PrefixVal.exists_litTrue, DescriptiveComplexity.SatOcc.prefixVal_prefixOr).

structure DescriptiveComplexity.SatOcc.PrefixVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (Z : A → A → Bool → Prop) : Prop

A prefix valuation of the assignment ν: a truth value for each occurrence of each clause, true exactly when the literal is true or the value at the preceding occurrence is, and true at the last occurrence of every clause; and there is no empty clause.

• step (c x : A) (s : Bool) : OccIn c x s → (Z c x s ↔ LitTrue ν x s ∨ ∃ (y : A) (t : Bool), SuccOcc c y t x s ∧ Z c y t)

  The value at an occurrence is the literal or the value before it.

• last (c x : A) (s : Bool) : MaxOcc c x s → Z c x s

  The value at the last occurrence of a clause is true.

• nonempty (c : A) : ¬EmptyCl c

  No clause is empty.

theorem DescriptiveComplexity.SatOcc.PrefixVal.iff_prefixOr {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {ν : A → Prop} {Z : A → A → Bool → Prop} (h : PrefixVal ν Z) (c x : A) (s : Bool) : OccIn c x s → (Z c x s ↔ PrefixOr ν c x s)

A prefix valuation is the truth of the prefix disjunctions.

theorem DescriptiveComplexity.SatOcc.PrefixVal.exists_litTrue {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {ν : A → Prop} {Z : A → A → Bool → Prop} (h : PrefixVal ν Z) {c : A} (hc : IsCl c) : ∃ (x : A) (s : Bool), OccIn c x s ∧ LitTrue ν x s

An assignment with a prefix valuation satisfies every clause.

theorem DescriptiveComplexity.SatOcc.prefixVal_prefixOr {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {ν : A → Prop} (hν : ∀ (c : A), IsCl c → ∃ (x : A) (s : Bool), OccIn c x s ∧ LitTrue ν x s) : PrefixVal ν (PrefixOr ν)

A satisfying assignment has a prefix valuation: the prefix disjunctions themselves.