Documentation

Complexitylib.DescriptiveComplexity.Circuit.Encoding

Circuit inputs in the existing structure encoding #

The computable layout reads the exact positions in encodeStruct, including the unary prefix offset. Unlike the abstract table numbering, it uses no classical choice. Compilation now evaluates the actual encoded structures. Circuit.Validity adds the constant-depth encoding check for arbitrary inputs.

source
def Complexity.DescriptiveComplexity.encodingLayout (V : Vocabulary) (card : ℕ) :
StructureInput V card (encodingLength V card)

Place relation and constant inputs at their actual encoded bit positions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.DescriptiveComplexity.encodedInput {V : Vocabulary} (A : DecFinStruct V) :
    BitString (encodingLength V A.card)

    View the encoder's list as a circuit input at its exact encoded length.

    Equations
    Instances For
      source
      theorem Complexity.DescriptiveComplexity.ofFn_encodedInput {V : Vocabulary} (A : DecFinStruct V) :
      List.ofFn (encodedInput A) = encodeStruct A

      Converting the circuit input vector to a list gives the original encoding exactly.

      source
      theorem Complexity.DescriptiveComplexity.encodedInput_represents {V : Vocabulary} (A : DecFinStruct V) :
      StructureInput.Represents A (encodingLayout V A.card) (encodedInput A)

      Every encoded structure supplies the relation and constant values required by compilation.

      source
      theorem Complexity.DescriptiveComplexity.Formula.encoded_expansion_sat {V : Vocabulary} {n : ℕ} (A : DecFinStruct V) (φ : Formula V n) (σ : Env A.card n) :
      AC0Formula.eval (encodedInput A) ((encodingLayout V A.card).compile φ σ) = true ↔ Sat A.toFinStruct σ φ

      The expansion reads the actual encoding correctly, for arbitrary open formulas.

      source
      theorem Complexity.DescriptiveComplexity.Sentence.encoded_expansion_models {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) :
      AC0Formula.eval (encodedInput A) ((encodingLayout V A.card).compile φ (emptyEnv A.card)) = true ↔ Models A.toFinStruct φ

      The sentence expansion computes truth on the existing structure encoding.

      source
      theorem Complexity.DescriptiveComplexity.Sentence.exists_encoding_circuit {V : Vocabulary} (φ : Sentence V) (card : ℕ) :
      ∃ (gates : ℕ) (c : Circuit Basis.unboundedAndOr (encodingLength V card) 1 gates), c.size = Polynomial.eval card (Formula.expansionPolynomial φ) ∧ c.depth ≤ Formula.size φ + 2 ∧ ∀ (input : BitString (encodingLength V card)), c.eval input 0 = AC0Formula.eval input ((encodingLayout V card).compile φ (emptyEnv card))

      At every universe size, one circuit computes the expansion on all encoded-length inputs. Correctness on encoded structures follows from encoded_expansion_models.