Documentation

CslibFrontier.Computability.Complexity.Problems.SAT.Planar.PathBounds

Bounds for shared incidence-path data #

Canonical path budgets, crossing counts, retained-gap counts, and 240-macrocell grid sides are independent of the emitted clause template. No output formula is defined here.

Main definitions #

Main results #

References #

These are the shared canonical incidence-path constructions and certificates.

source
def Cslib.Complexity.SAT.PlanarCompile.linkCount (φ : Logic.PL.CNF ℕ) :
ℕ

Number of retained path gaps before the final step into each source clause.

Instances For
    source
    theorem Cslib.Complexity.SAT.PlanarCompile.crossingSites_length_le (φ : Logic.PL.CNF ℕ) :
    (crossingSites φ).length ≤ 2 * φ.vars.length ^ 2

    Selected crossing sites form a sublist of the quadratic canonical cover after deduplication. The bound counts all source literal incidences, including repetitions.

    source
    theorem Cslib.Complexity.SAT.PlanarCompile.paths_length (φ : Logic.PL.CNF ℕ) :
    (paths φ).length = φ.vars.length

    There is one unit path per original literal incidence.

    source
    theorem Cslib.Complexity.SAT.PlanarCompile.path_length_le {φ : Logic.PL.CNF ℕ} {r : Orthogonal.Route} (hr : r ∈ paths φ) :
    List.length r ≤ 5 * budget φ + 1

    The bounded enumerator emits at most five segment budgets plus the final endpoint. This unconditional bound also applies to inputs that fail the degree-three restriction.

    source
    theorem Cslib.Complexity.SAT.PlanarCompile.occurrencePath_length_le (φ : Logic.PL.CNF ℕ) (o : Logic.PL.Occurrence ℕ) :
    List.length (occurrencePath φ o) ≤ 5 * budget φ + 1

    Indexed access to a path obeys the same bound, including the empty fallback.

    source
    theorem Cslib.Complexity.SAT.PlanarCompile.linkCount_le (φ : Logic.PL.CNF ℕ) :
    linkCount φ ≤ φ.vars.length * (5 * budget φ + 1)

    There are quadratically many links, even before checking the source restrictions.

    source
    def Cslib.Complexity.SAT.PlanarCompile.gridWidth (φ : Logic.PL.CNF ℕ) :
    ℕ

    Horizontal side of the actual tiled drawing, including its last square.

    Instances For
      source
      def Cslib.Complexity.SAT.PlanarCompile.gridHeight (φ : Logic.PL.CNF ℕ) :
      ℕ

      Vertical side of the actual tiled drawing, including its last square.

      Instances For
        source
        theorem Cslib.Complexity.SAT.PlanarCompile.gridWidth_le (φ : Logic.PL.CNF ℕ) :
        gridWidth φ ≤ 1920 * (φ.numVars + List.length φ + φ.vars.length + 1)

        The horizontal grid side is at most 1920 times the source incidence size plus one.

        source
        theorem Cslib.Complexity.SAT.PlanarCompile.gridHeight_le (φ : Logic.PL.CNF ℕ) :
        gridHeight φ ≤ 1920 * (φ.numVars + List.length φ + φ.vars.length + 1)

        The vertical grid side is at most 1920 times the source incidence size plus one.