The Tseitin encoding determines its gate variables #
Two facts about the encoding of DescriptiveComplexity.Problems.Sat.Tseitin that a
decision reduction does not need and a parsimonious one does: they say that a
model of the encoding carries no information beyond the block assignment it
induces.
DescriptiveComplexity.Tseitin.gates_unique: a valuation of the position variables satisfying every gate is the canonical one, at every position and not only at the root (DescriptiveComplexity.Tseitin.gates_realize);DescriptiveComplexity.Tseitin.litSem_varCanon: a propositional variable occurring in a clause sits at a canonically padded tuple, of the length its kind prescribes (DescriptiveComplexity.Tseitin.VarCanon). So the non-canonical tuples are not variables of the encoding at all.
theorem
DescriptiveComplexity.Tseitin.gates_unique
{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 determine the valuation: a valuation of the position variables satisfying every gate assigns to every position the truth value of its subformula.
Dependency graph
def
DescriptiveComplexity.Tseitin.VarCanon
{L : FirstOrder.Language}
{B : SOBlock}
{A : Type}
{D : ℕ}
[LE A]
{n : ℕ}
{f : (L.sum B.lang).BoundedFormula Empty n}
(v : B.ι ⊕ (m' : ℕ) × NodeAt f m')
(x : Fin D → A)
:
The tuple x is canonical for the propositional variable indexed by v:
padded from the arity on for a block variable, from the context length on for a
position variable.
Equations
Instances For
Dependency graph
theorem
DescriptiveComplexity.Tseitin.litSem_varCanon
{L : FirstOrder.Language}
{B : SOBlock}
{A : Type}
{D : ℕ}
[L.Structure A]
[LE A]
(s : Bool)
{n : ℕ}
(f : (L.sum B.lang).BoundedFormula Empty n)
(h : maxCtx f ≤ D)
{m : ℕ}
(p : NodeAt f m)
(k : Fin 3)
(u : Fin D → A)
(v : B.ι ⊕ (m' : ℕ) × NodeAt f m')
(x : Fin D → A)
:
IsClauseSem f h p k u → LitSem s f h p k u v x → VarCanon v x
Variables of the encoding sit at canonical tuples: a literal of a clause of the Tseitin encoding is a propositional variable at a tuple that is canonical for it.