The Tseitin encoding of a first-order kernel: semantic layer

Machinery for the hardness half of the Cook–Levin theorem (Cook 1971; Levin 1973; DescriptiveComplexity.sat_hard_of_sigmaSODefinable, in DescriptiveComplexity.Problems.Sat.Hardness): the generic, machine-free reduction of any existential-second-order definable problem to SAT (via a Tseitin (Tseitin 1968) encoding), in the style of Dahlhaus (Dahlhaus 1983). Given the first-order kernel φ (a sentence over the input vocabulary expanded by one second-order block), the produced CNF instance has

• one propositional variable per relation variable i of the block and tuple ā (“ā ∈ Rᵢ”), and one per subformula position p of φ and context tuple w (“the subformula at p holds under w”);
• Tseitin-style clauses per subformula position, forcing the position variables to compute the truth value of their subformulas bottom-up.

This file contains the semantic part of the construction, independent of the FO formulas defining the CNF instance inside the input structure:

• DescriptiveComplexity.Tseitin.NodeAt f m: the type of subformula positions of f with context length m (the root is uniformly reachable via DescriptiveComplexity.Tseitin.rootAt);
• DescriptiveComplexity.Tseitin.Gates: a valuation of the position variables computes truth values correctly at every position (“all Tseitin gates hold”);
• DescriptiveComplexity.Tseitin.canonVal, the canonical valuation by actual truth values, which satisfies all gates (DescriptiveComplexity.Tseitin.gates_canonVal), and the converse reading (DescriptiveComplexity.Tseitin.gates_realize): any valuation satisfying the gates assigns the root its actual truth value;
• DescriptiveComplexity.Tseitin.IsClauseSem / DescriptiveComplexity.Tseitin.LitSem: the clauses of the encoding and their literals, as semantic predicates on tuples of a fixed length D padded with minimal elements (junk tuples are excluded by canonicity conditions);
• the main equivalence DescriptiveComplexity.Tseitin.satCond_iff_gates: a valuation satisfies every clause iff the induced (padding-invariant) valuation satisfies every gate.

The corresponding first-order formulas and their realization lemmas are in DescriptiveComplexity.Problems.Sat.TseitinFormulas.

Subformula positions

def DescriptiveComplexity.Tseitin.NodeAt {L' : FirstOrder.Language} {n : ℕ} : L'.BoundedFormula Empty n → ℕ → Type

The type of subformula positions (“nodes”) of f with context length m: positions at which the subformula has m free de Bruijn variables. The family is indexed by the context length so that all node-dependent data (valuations, clauses) can be typed uniformly, without a dependent context function.

Equations

• DescriptiveComplexity.Tseitin.NodeAt FirstOrder.Language.BoundedFormula.falsum x✝ = PLift (x✝¹ = x✝)
• DescriptiveComplexity.Tseitin.NodeAt (FirstOrder.Language.BoundedFormula.equal t₁ t₂) x✝ = PLift (x✝¹ = x✝)
• DescriptiveComplexity.Tseitin.NodeAt (FirstOrder.Language.BoundedFormula.rel R ts) x✝ = PLift (x✝¹ = x✝)
• DescriptiveComplexity.Tseitin.NodeAt (f₁.imp f₂) x✝ = (PLift (x✝¹ = x✝) ⊕ DescriptiveComplexity.Tseitin.NodeAt f₁ x✝ ⊕ DescriptiveComplexity.Tseitin.NodeAt f₂ x✝)
• DescriptiveComplexity.Tseitin.NodeAt f.all x✝ = (PLift (x✝¹ = x✝) ⊕ DescriptiveComplexity.Tseitin.NodeAt f x✝)

def DescriptiveComplexity.Tseitin.rootAt {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) : NodeAt f n

The root position of a formula.

Equations

• DescriptiveComplexity.Tseitin.rootAt FirstOrder.Language.BoundedFormula.falsum = { down := ⋯ }
• DescriptiveComplexity.Tseitin.rootAt (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = { down := ⋯ }
• DescriptiveComplexity.Tseitin.rootAt (FirstOrder.Language.BoundedFormula.rel R ts) = { down := ⋯ }
• DescriptiveComplexity.Tseitin.rootAt (f₁.imp f₂) = Sum.inl { down := ⋯ }
• DescriptiveComplexity.Tseitin.rootAt f.all = Sum.inl { down := ⋯ }

def DescriptiveComplexity.Tseitin.isRootB {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) {m : ℕ} : NodeAt f m → Bool

Whether a position is the root, as a Boolean (usable inside formula definitions, where positions of a variable formula cannot be pattern-matched).

Equations

• DescriptiveComplexity.Tseitin.isRootB FirstOrder.Language.BoundedFormula.falsum x✝ = true
• DescriptiveComplexity.Tseitin.isRootB (FirstOrder.Language.BoundedFormula.equal t₁ t₂) x✝ = true
• DescriptiveComplexity.Tseitin.isRootB (FirstOrder.Language.BoundedFormula.rel R ts) x✝ = true
• DescriptiveComplexity.Tseitin.isRootB (f₁.imp f₂) x✝ = Sum.isLeft x✝
• DescriptiveComplexity.Tseitin.isRootB f.all x✝ = Sum.isLeft x✝

theorem DescriptiveComplexity.Tseitin.isRootB_iff {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) {m : ℕ} (p : NodeAt f m) : isRootB f p = true ↔ ⟨m, p⟩ = ⟨n, rootAt f⟩

A position is the root iff isRootB says so; in that case its context length is the formula's own index. Stated as an equality of dependent pairs.

theorem DescriptiveComplexity.Tseitin.sigma_map_eq_iff {β β' : ℕ → Type} (F : (m : ℕ) → β m → β' m) (hF : ∀ (m : ℕ), Function.Injective (F m)) {m₁ m₂ : ℕ} (a : β m₁) (b : β m₂) : ⟨m₁, F m₁ a⟩ = ⟨m₂, F m₂ b⟩ ↔ ⟨m₁, a⟩ = ⟨m₂, b⟩

Equality of dependent pairs through a fiberwise injective map.

def DescriptiveComplexity.Tseitin.maxCtx {L' : FirstOrder.Language} {n : ℕ} : L'.BoundedFormula Empty n → ℕ

The largest context length occurring in a formula.

Equations

• DescriptiveComplexity.Tseitin.maxCtx FirstOrder.Language.BoundedFormula.falsum = x✝
• DescriptiveComplexity.Tseitin.maxCtx (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = x✝
• DescriptiveComplexity.Tseitin.maxCtx (FirstOrder.Language.BoundedFormula.rel R ts) = x✝
• DescriptiveComplexity.Tseitin.maxCtx (f₁.imp f₂) = max (DescriptiveComplexity.Tseitin.maxCtx f₁) (DescriptiveComplexity.Tseitin.maxCtx f₂)
• DescriptiveComplexity.Tseitin.maxCtx f.all = DescriptiveComplexity.Tseitin.maxCtx f

theorem DescriptiveComplexity.Tseitin.le_maxCtx {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) : n ≤ maxCtx f

A formula's own index is a context length, hence bounded by maxCtx.

theorem DescriptiveComplexity.Tseitin.nodeAt_le_maxCtx {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) {m : ℕ} : ∀ (a : NodeAt f m), m ≤ maxCtx f

Context lengths of actual positions are bounded by maxCtx.

instance DescriptiveComplexity.Tseitin.finite_sigma_nodeAt {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) : Finite ((m : ℕ) × NodeAt f m)

There are finitely many positions in a formula.

Terms of the expanded language

def DescriptiveComplexity.Tseitin.termToL {L : FirstOrder.Language} {B : SOBlock} {α : Type} : (L.sum B.lang).Term α → L.Term α

A term of the language expanded by a (relational) block is a term of the base language.

Equations

• DescriptiveComplexity.Tseitin.termToL (FirstOrder.Language.var a) = FirstOrder.Language.var a
• DescriptiveComplexity.Tseitin.termToL (FirstOrder.Language.func (Sum.inl f_2) ts) = FirstOrder.Language.func f_2 fun (i : Fin l) => DescriptiveComplexity.Tseitin.termToL (ts i)
• DescriptiveComplexity.Tseitin.termToL (FirstOrder.Language.func (Sum.inr f_2) ts) = isEmptyElim f_2

theorem DescriptiveComplexity.Tseitin.sumInl_onTerm_termToL {L : FirstOrder.Language} {B : SOBlock} {α : Type} (t : (L.sum B.lang).Term α) : FirstOrder.Language.LHom.sumInl.onTerm (termToL t) = t

Reembedding termToL into the expanded language gives the term back.

theorem DescriptiveComplexity.Tseitin.realize_termToL {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] [(L.sum B.lang).Structure A] [FirstOrder.Language.LHom.sumInl.IsExpansionOn A] {α : Type} (t : (L.sum B.lang).Term α) (v : α → A) : FirstOrder.Language.Term.realize v (termToL t) = FirstOrder.Language.Term.realize v t

Realization of termToL in the base structure agrees with realization of the term in any expansion.

Gates: correctness of a valuation of the position variables

@[instance_reducible]

def DescriptiveComplexity.Tseitin.assignStructure {A : Type} (L : FirstOrder.Language) [L.Structure A] {B : SOBlock} (μ : B.Assignment A) : (L.sum B.lang).Structure A

The expansion of an L-structure by a block assignment.

Equations

• DescriptiveComplexity.Tseitin.assignStructure L μ = inferInstance

def DescriptiveComplexity.Tseitin.RealizeWith {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) (w : Fin n → A) : Prop

Realization of a kernel formula in the expansion of an L-structure by a block assignment.

Equations

• DescriptiveComplexity.Tseitin.RealizeWith μ f w = f.Realize (fun (a : Empty) => isEmptyElim a) w

def DescriptiveComplexity.Tseitin.eqGuard {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (t₁ t₂ : (L.sum B.lang).Term (Empty ⊕ Fin m)) (w : Fin m → A) : Prop

The truth value of an equality atom of the kernel under a context tuple.

Equations

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

def DescriptiveComplexity.Tseitin.relGuard {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] {m l : ℕ} (r : L.Relations l) (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin m)) (w : Fin m → A) : Prop

The truth value of an input-relation atom of the kernel under a context tuple.

Equations

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

def DescriptiveComplexity.Tseitin.blockAtom {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {m l : ℕ} (r : B.lang.Relations l) (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin m)) (w : Fin m → A) : Prop

The truth value of a block-variable atom of the kernel under an assignment and a context tuple.

Equations

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

def DescriptiveComplexity.Tseitin.atomHolds {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {m l : ℕ} (R : (L.sum B.lang).Relations l) (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin m)) (w : Fin m → A) : Prop

The truth value of an arbitrary atom of the kernel.

Equations

• DescriptiveComplexity.Tseitin.atomHolds μ (Sum.inl r) ts w = DescriptiveComplexity.Tseitin.relGuard r ts w
• DescriptiveComplexity.Tseitin.atomHolds μ (Sum.inr r) ts w = DescriptiveComplexity.Tseitin.blockAtom μ r ts w

@[reducible, inline]

abbrev DescriptiveComplexity.Tseitin.NodeVal (A : Type) {L' : FirstOrder.Language} {n : ℕ} (f : L'.BoundedFormula Empty n) : Type

A valuation of the position variables of a formula: a truth value for every position and context tuple.

Equations

• DescriptiveComplexity.Tseitin.NodeVal A f = ((m : ℕ) → DescriptiveComplexity.Tseitin.NodeAt f m → (Fin m → A) → Prop)

def DescriptiveComplexity.Tseitin.Gates {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) : NodeVal A f → Prop

All Tseitin gates of a formula hold under a valuation of its position variables: at every position, the valuation relates to the valuations at the children (or to the atom's truth value) as dictated by the connective. A valuation satisfying all gates computes actual truth values (DescriptiveComplexity.Tseitin.gates_realize).

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Tseitin.Gates μ FirstOrder.Language.BoundedFormula.falsum ν = ∀ (w : Fin x✝ → A), ¬ν x✝ { down := ⋯ } w
• DescriptiveComplexity.Tseitin.Gates μ (FirstOrder.Language.BoundedFormula.equal t₁ t₂) ν = ∀ (w : Fin x✝ → A), ν x✝ { down := ⋯ } w ↔ DescriptiveComplexity.Tseitin.eqGuard t₁ t₂ w
• DescriptiveComplexity.Tseitin.Gates μ (FirstOrder.Language.BoundedFormula.rel R ts) ν = ∀ (w : Fin x✝ → A), ν x✝ { down := ⋯ } w ↔ DescriptiveComplexity.Tseitin.atomHolds μ R ts w

def DescriptiveComplexity.Tseitin.canonVal {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) : NodeVal A f

The canonical valuation: each position variable receives the truth value of its subformula.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Tseitin.canonVal μ FirstOrder.Language.BoundedFormula.falsum x✝² x✝ x✝¹ = False
• DescriptiveComplexity.Tseitin.canonVal μ (f₁.imp f₂) x✝¹ (Sum.inl h) x✝ = DescriptiveComplexity.Tseitin.RealizeWith μ (f₁.imp f₂) (x✝ ∘ Fin.cast ⋯)
• DescriptiveComplexity.Tseitin.canonVal μ (f₁.imp f₂) x✝¹ (Sum.inr (Sum.inl q)) x✝ = DescriptiveComplexity.Tseitin.canonVal μ f₁ x✝¹ q x✝
• DescriptiveComplexity.Tseitin.canonVal μ (f₁.imp f₂) x✝¹ (Sum.inr (Sum.inr q)) x✝ = DescriptiveComplexity.Tseitin.canonVal μ f₂ x✝¹ q x✝
• DescriptiveComplexity.Tseitin.canonVal μ f.all x✝¹ (Sum.inl h) x✝ = DescriptiveComplexity.Tseitin.RealizeWith μ f.all (x✝ ∘ Fin.cast ⋯)
• DescriptiveComplexity.Tseitin.canonVal μ f.all x✝¹ (Sum.inr q) x✝ = DescriptiveComplexity.Tseitin.canonVal μ f x✝¹ q x✝

theorem DescriptiveComplexity.Tseitin.canonVal_rootAt {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) (w : Fin n → A) : canonVal μ f n (rootAt f) w ↔ RealizeWith μ f w

The canonical valuation at the root is the truth value of the whole formula.

Unfolding RealizeWith

theorem DescriptiveComplexity.Tseitin.realizeWith_falsum {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (w : Fin n → A) : ¬RealizeWith μ FirstOrder.Language.BoundedFormula.falsum w

theorem DescriptiveComplexity.Tseitin.realizeWith_equal {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (t₁ t₂ : (L.sum B.lang).Term (Empty ⊕ Fin n)) (w : Fin n → A) : RealizeWith μ (FirstOrder.Language.BoundedFormula.equal t₁ t₂) w ↔ eqGuard t₁ t₂ w

theorem DescriptiveComplexity.Tseitin.realizeWith_rel {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n l : ℕ} (R : (L.sum B.lang).Relations l) (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin n)) (w : Fin n → A) : RealizeWith μ (FirstOrder.Language.BoundedFormula.rel R ts) w ↔ atomHolds μ R ts w

theorem DescriptiveComplexity.Tseitin.realizeWith_imp {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (f₁ f₂ : (L.sum B.lang).BoundedFormula Empty n) (w : Fin n → A) : RealizeWith μ (f₁.imp f₂) w ↔ RealizeWith μ f₁ w → RealizeWith μ f₂ w

theorem DescriptiveComplexity.Tseitin.realizeWith_all {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty (n + 1)) (w : Fin n → A) : RealizeWith μ f.all w ↔ ∀ (a : A), RealizeWith μ f (Fin.snoc w a)

Gates compute truth values

theorem DescriptiveComplexity.Tseitin.gates_realize {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) (ν : NodeVal A f) : Gates μ f ν → ∀ (w : Fin n → A), ν n (rootAt f) w ↔ RealizeWith μ f w

Any valuation satisfying all gates assigns to the root the truth value of the formula.

theorem DescriptiveComplexity.Tseitin.gates_canonVal {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] (μ : B.Assignment A) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) : Gates μ f (canonVal μ f)

The canonical valuation satisfies all gates.

The clauses of the encoding and their literals

def DescriptiveComplexity.Tseitin.atomLit {L : FirstOrder.Language} {B : SOBlock} {A : Type} {D : ℕ} [L.Structure A] [LE A] {m l : ℕ} (ts : Fin l → (L.sum B.lang).Term (Empty ⊕ Fin m)) (w : Fin m → A) (x : Fin D → A) : Prop

The literal tuple of a block-variable atom: canonical, with the atom's term values as prefix.

Equations

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

def DescriptiveComplexity.Tseitin.IsClauseSem {L : FirstOrder.Language} {B : SOBlock} {A : Type} {D : ℕ} [L.Structure A] [LE A] {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) : maxCtx f ≤ D → {m : ℕ} → NodeAt f m → Fin 3 → (Fin D → A) → Prop

The clauses of the Tseitin encoding, as a predicate on positions, clause kinds (Fin 3) and canonical D-tuples:

• falsum node at context w: kind 0, the unit clause ¬v(p, w);
• equal/input-relation node: kind 0, the unit clause v(p, w), present when the atom holds under w; kind 1, the unit clause ¬v(p, w), present otherwise;
• block-variable node: kind 0, ¬v(p, w) ∨ R(ā); kind 1, v(p, w) ∨ ¬R(ā);
• imp node with children a, b: kind 0, ¬v(p, w) ∨ ¬a(w) ∨ b(w); kind 1, v(p, w) ∨ a(w); kind 2, v(p, w) ∨ ¬b(w);
• all node with child c: kind 0 (indexed by extended tuples w ⌢ a), ¬v(p, w) ∨ c(w ⌢ a); kind 1, the wide clause v(p, w) ∨ ⋁_a ¬c(w ⌢ a).

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Tseitin.IsClauseSem FirstOrder.Language.BoundedFormula.falsum x_7 x_4 x_2 x_3 = (x_2 = 0 ∧ DescriptiveComplexity.Canon x x_3)
• DescriptiveComplexity.Tseitin.IsClauseSem (FirstOrder.Language.BoundedFormula.rel (Sum.inr val) ts) h_2 x_8 x_2 x_3 = (DescriptiveComplexity.Canon x x_3 ∧ (x_2 = 0 ∨ x_2 = 1))
• DescriptiveComplexity.Tseitin.IsClauseSem (f₁.imp f₂) h (Sum.inl h_1) x_2 x_3 = DescriptiveComplexity.Canon x x_3
• DescriptiveComplexity.Tseitin.IsClauseSem (f₁.imp f₂) h (Sum.inr (Sum.inl q)) x_2 x_3 = DescriptiveComplexity.Tseitin.IsClauseSem f₁ ⋯ q x_2 x_3
• DescriptiveComplexity.Tseitin.IsClauseSem (f₁.imp f₂) h (Sum.inr (Sum.inr q)) x_2 x_3 = DescriptiveComplexity.Tseitin.IsClauseSem f₂ ⋯ q x_2 x_3
• DescriptiveComplexity.Tseitin.IsClauseSem f.all h (Sum.inl h_1) x_2 x_3 = (x_2 = 0 ∧ DescriptiveComplexity.Canon (x + 1) x_3 ∨ x_2 = 1 ∧ DescriptiveComplexity.Canon x x_3)
• DescriptiveComplexity.Tseitin.IsClauseSem f.all h (Sum.inr q) x_2 x_3 = DescriptiveComplexity.Tseitin.IsClauseSem f h q x_2 x_3

def DescriptiveComplexity.Tseitin.LitSem {L : FirstOrder.Language} {B : SOBlock} {A : Type} {D : ℕ} [L.Structure A] [LE A] (s : Bool) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) : maxCtx f ≤ D → {m : ℕ} → NodeAt f m → Fin 3 → (Fin D → A) → B.ι ⊕ (m' : ℕ) × NodeAt f m' → (Fin D → A) → Prop

The literals of the clauses of the Tseitin encoding: LitSem s f h p k u v x states that the propositional variable indexed by v (a block variable index or a position) at tuple x occurs with sign s in the clause (p, k, u). The clause-existence guards of DescriptiveComplexity.Tseitin.IsClauseSem are not repeated here.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Tseitin.LitSem s FirstOrder.Language.BoundedFormula.falsum x_9 x_5 x_2 x_3 v x_4 = (s = false ∧ x_2 = 0 ∧ v = Sum.inr ⟨x, { down := ⋯ }⟩ ∧ x_4 = x_3)
• DescriptiveComplexity.Tseitin.LitSem s (f₁.imp f₂) h (Sum.inr (Sum.inl q)) x_2 x_3 (Sum.inl i) x_4 = DescriptiveComplexity.Tseitin.LitSem s f₁ ⋯ q x_2 x_3 (Sum.inl i) x_4
• DescriptiveComplexity.Tseitin.LitSem s (f₁.imp f₂) h (Sum.inr (Sum.inl q)) x_2 x_3 v x_4 = False
• DescriptiveComplexity.Tseitin.LitSem s (f₁.imp f₂) h (Sum.inr (Sum.inr q)) x_2 x_3 (Sum.inl i) x_4 = DescriptiveComplexity.Tseitin.LitSem s f₂ ⋯ q x_2 x_3 (Sum.inl i) x_4
• DescriptiveComplexity.Tseitin.LitSem s (f₁.imp f₂) h (Sum.inr (Sum.inr q)) x_2 x_3 v x_4 = False
• DescriptiveComplexity.Tseitin.LitSem s f.all h (Sum.inr q) x_2 x_3 (Sum.inl i) x_4 = DescriptiveComplexity.Tseitin.LitSem s f h q x_2 x_3 (Sum.inl i) x_4
• DescriptiveComplexity.Tseitin.LitSem s f.all h (Sum.inr q) x_2 x_3 (Sum.inr ⟨m', Sum.inr q'⟩) x_4 = DescriptiveComplexity.Tseitin.LitSem s f h q x_2 x_3 (Sum.inr ⟨m', q'⟩) x_4
• DescriptiveComplexity.Tseitin.LitSem s f.all h (Sum.inr q) x_2 x_3 v x_4 = False

Clause satisfaction is gate satisfaction

def DescriptiveComplexity.Tseitin.SatCond {L : FirstOrder.Language} {B : SOBlock} {A : Type} {D : ℕ} [L.Structure A] [LinearOrder A] {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) (hctx : maxCtx f ≤ D) (tv : B.ι ⊕ (m : ℕ) × NodeAt f m → (Fin D → A) → Prop) : Prop

Every clause of the encoding contains a literal made true by the valuation tv of the propositional variables.

Equations

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

def DescriptiveComplexity.Tseitin.padAssign {L : FirstOrder.Language} {B : SOBlock} {A : Type} {D : ℕ} (a₀ : A) {n : ℕ} {f : (L.sum B.lang).BoundedFormula Empty n} (tv : B.ι ⊕ (m : ℕ) × NodeAt f m → (Fin D → A) → Prop) : B.Assignment A

The block assignment read off a valuation of the propositional variables, on padded tuples.

Equations

• DescriptiveComplexity.Tseitin.padAssign a₀ tv i a = tv (Sum.inl i) (DescriptiveComplexity.pad a₀ a)

def DescriptiveComplexity.Tseitin.padVal {L : FirstOrder.Language} {B : SOBlock} {A : Type} {D : ℕ} (a₀ : A) {n : ℕ} {f : (L.sum B.lang).BoundedFormula Empty n} (tv : B.ι ⊕ (m : ℕ) × NodeAt f m → (Fin D → A) → Prop) : NodeVal A f

The position valuation read off a valuation of the propositional variables, on padded tuples.

Equations

• DescriptiveComplexity.Tseitin.padVal a₀ tv m q w = tv (Sum.inr ⟨m, q⟩) (DescriptiveComplexity.pad a₀ w)

theorem DescriptiveComplexity.Tseitin.satCond_iff_gates {L : FirstOrder.Language} {B : SOBlock} {A : Type} {D : ℕ} [L.Structure A] [LinearOrder A] {a₀ : A} (h₀ : IsBot a₀) (harity : ∀ (i : B.ι), B.arity i ≤ D) {n : ℕ} (f : (L.sum B.lang).BoundedFormula Empty n) (hctx : maxCtx f ≤ D) (tv : B.ι ⊕ (m : ℕ) × NodeAt f m → (Fin D → A) → Prop) : SatCond f hctx tv ↔ Gates (padAssign a₀ tv) f (padVal a₀ tv)

Clause satisfaction is gate satisfaction: a valuation of the propositional variables makes every clause of the Tseitin encoding true iff the valuation it induces on positions (through canonical padding) satisfies every gate, with the block variables read off the atom variables.