Documentation

DescriptiveComplexity.Problems.ThreeColorability.Counting

#3-Colorability: counting the proper 3-colorings #

The counting version of DescriptiveComplexity.ThreeCol: the number of proper colorings of a graph with the three colors Fin 3 (DescriptiveComplexity.SharpThreeCol). It is in #P (DescriptiveComplexity.sharpThreeCol_mem_sharpP), the coloring being three guessed color classes partitioning the vertices; its one-call completeness is in DescriptiveComplexity.Problems.ThreeColorability.CountDraw.

source
noncomputable def DescriptiveComplexity.colExclusiveClause :
(kColSOLang 3).Sentence

Kernel clause: no vertex is in two color classes.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.sharpThreeColKernel :
    (kColSOLang 3).Sentence

    The kernel of #3-Colorability: the color classes partition the vertices and no edge stays inside a class.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.realize_sharpThreeColKernel {V : Type} [FirstOrder.Language.graph.Structure V] (ρ : (colorGuessBlock 3).Assignment V) :
      V ⊨ sharpThreeColKernel ↔ ((∀ (x : V), ∃ (i : Fin 3), ρ i ![x]) ∧ ∀ (x y : V), FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y] → ∀ (i : Fin 3), ¬(ρ i ![x] ∧ ρ i ![y])) ∧ ∀ (x : V) (i j : Fin 3), ρ i ![x] → ρ j ![x] → i = j
      Dependency graph
      source
      def DescriptiveComplexity.colorAssign {V : Type} (χ : V → Fin 3) :
      (colorGuessBlock 3).Assignment V

      A 3-coloring, as an assignment of the three color classes.

      Equations
      Instances For
        Dependency graph
        source
        noncomputable def DescriptiveComplexity.threeColEquiv (V : Type) [FirstOrder.Language.graph.Structure V] :
        { ρ : (colorGuessBlock 3).Assignment V // V ⊨ sharpThreeColKernel } ≃ { χ : V → Fin 3 // ∀ (x y : V), FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y] → χ x ≠ χ y }

        The proper 3-colorings are the witnesses of the kernel.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Dependency graph
          source
          noncomputable def DescriptiveComplexity.SharpThreeCol :
          CountingProblem FirstOrder.Language.graph

          #3-Colorability: the number of proper colorings of a graph with three colors.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Dependency graph
            source
            theorem DescriptiveComplexity.sharpThreeCol_mem_sharpP :
            SharpP.Mem SharpThreeCol

            #3-Colorability is in #P.

            Dependency graph