Documentation

Complexitylib.DescriptiveComplexity.Problems.Coloring

Bipartiteness as an existential second-order query #

The graph vocabulary describes arbitrary directed graphs, including loops. A bipartition assigns a Boolean color to each vertex, with different colors at the ends of every directed edge. Symmetry is not required; a loop prevents a coloring.

The sentence ∃X ∀x ∀y (E(x,y) → (X(x) ↔ ¬X(y))) defines this query. This is the example in Senellart and Gnatenko (2026), Section 2.1, https://arxiv.org/abs/2609.18261. We prove agreement with an ordinary Boolean coloring, rather than defining the query as satisfaction of its witness. No NP membership or hardness statement is claimed here. checkBipartition executes the matrix on a supplied Boolean coloring and is proved to accept exactly the colorings separating every directed edge. The general binary certificate checker agrees with it when the certificate lists the vertex colors, one bit per vertex.

source
def Complexity.DescriptiveComplexity.GraphQuery.Edge (A : FinStruct Vocabulary.graph) (x y : Fin A.card) :
Prop

There is an edge from x to y in a graph structure.

Equations
Instances For
    source
    def Complexity.DescriptiveComplexity.GraphQuery.Bipartite :
    BooleanQuery Vocabulary.graph

    A Boolean coloring separates the endpoints of every directed edge.

    Equations
    Instances For
      source
      theorem Complexity.DescriptiveComplexity.GraphQuery.bipartite_of_no_edges {A : FinStruct Vocabulary.graph} (h : ∀ (x y : Fin A.card), ¬Edge A x y) :
      Bipartite A

      A graph without edges has a constant Boolean coloring.

      source
      theorem Complexity.DescriptiveComplexity.GraphQuery.not_bipartite_of_loop {A : FinStruct Vocabulary.graph} {x : Fin A.card} (h : Edge A x x) :
      ¬Bipartite A

      A self-loop rules out a Boolean bipartition.

      source
      def Complexity.DescriptiveComplexity.GraphQuery.bipartiteMatrix :
      SOFormula Vocabulary.graph [1] 2

      The open FO matrix: adjacent vertices disagree on the unary relation variable.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.DescriptiveComplexity.GraphQuery.bipartiteSentence :
        SOSentence Vocabulary.graph

        Guess one unary relation, then check every pair of vertices.

        Equations
        Instances For
          source
          theorem Complexity.DescriptiveComplexity.GraphQuery.bipartiteSentence_isExistSO :
          SOFormula.IsExistSO bipartiteSentence

          This witness has one existential SO quantifier and an FO matrix.

          source
          theorem Complexity.DescriptiveComplexity.GraphQuery.bipartiteMatrix_sat (A : FinStruct Vocabulary.graph) (σ : Env A.card 2) (S : (Fin 1 → Fin A.card) → Prop) :
          SOFormula.Sat A σ (rCons S (emptyREnv A.card)) bipartiteMatrix ↔ Edge A (σ 0) (σ 1) → ((S fun (x : Fin 1) => σ 0) ↔ ¬S fun (x : Fin 1) => σ 1)

          Semantics of the open matrix, independent of the choice of variable environment.

          source
          theorem Complexity.DescriptiveComplexity.GraphQuery.bipartiteSentence_models (A : FinStruct Vocabulary.graph) :
          SOSentence.Models A bipartiteSentence ↔ Bipartite A

          The logical witness defines exactly the Boolean-coloring query.

          source
          theorem Complexity.DescriptiveComplexity.GraphQuery.bipartite_existSODefinable :
          ExistSODefinable Bipartite

          Bipartiteness is existential second-order definable.

          source
          def Complexity.DescriptiveComplexity.GraphQuery.checkBipartition (A : DecFinStruct Vocabulary.graph) (color : Fin A.card → Bool) :
          Bool

          Check a supplied Boolean bipartition by evaluating the sentence's FO matrix.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Complexity.DescriptiveComplexity.GraphQuery.checkBipartition_eq_true (A : DecFinStruct Vocabulary.graph) (color : Fin A.card → Bool) :
            checkBipartition A color = true ↔ ∀ (x y : Fin A.toFinStruct.card), Edge A.toFinStruct x y → color x ≠ color y

            The executable witness checker accepts exactly the proper Boolean colorings.

            source
            theorem Complexity.DescriptiveComplexity.GraphQuery.exists_checkBipartition_iff (A : DecFinStruct Vocabulary.graph) :
            (∃ (color : Fin A.card → Bool), checkBipartition A color = true) ↔ Bipartite A.toFinStruct

            A graph is bipartite exactly when the executable checker accepts some coloring.

            source
            theorem Complexity.DescriptiveComplexity.GraphQuery.checkEncoded_bipartite_colors (A : DecFinStruct Vocabulary.graph) (color : Fin A.card → Bool) :
            bipartiteSentence.checkEncoded bipartiteSentence_isExistSO (encodeStruct A) (List.ofFn color) = checkBipartition A color

            The binary certificate for bipartiteness is exactly one color bit per vertex.

            source
            theorem Complexity.DescriptiveComplexity.GraphQuery.exists_checkEncoded_bipartite_iff (input : List Bool) :
            (∃ (certificate : List Bool), bipartiteSentence.checkEncoded bipartiteSentence_isExistSO input certificate = true) ↔ input ∈ queryLanguage Bipartite

            The binary certificate checker characterizes the ordinary bipartite-graph language.

            source
            theorem Complexity.DescriptiveComplexity.GraphQuery.bipartite_orderIndependent :
            Bipartite.IsOrderIndependent

            Relabeling vertices preserves bipartiteness.

            source
            theorem Complexity.DescriptiveComplexity.GraphQuery.existSODefinable_of_reduces_bipartite {V : Vocabulary} {Q : BooleanQuery V} (h : FOReduces Q Bipartite) :
            ExistSODefinable Q

            Every query FO-reducible to bipartiteness has an existential SO witness.