Lax Lean Archive

Binary encoding of graph decision instances

Lax222097.GraphEncoding · concepts/Lax222097/GraphEncoding.lean · lax-222097

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    An instance consists of a finite simple graph on {0,…,n−1}\{0,\ldots,n-1\} and a threshold kk. Its encoding is 1n01^n0, followed by the n2n^2 adjacency-matrix bits in row order, followed by 1k01^k0. Polynomial running time is measured in the length of this word.

    Concept map
    2 concepts; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Clique
    2import Mathlib.Data.List.FinRange
    3import Lax434930.PolynomialTime
    4
    5/-!
    6---
    7title: Binary encoding of graph decision instances
    8type: definition
    9---
    10An instance consists of a finite simple graph on {0,…,n−1}\{0,\ldots,n-1\} and a
    11threshold kk. Its encoding is 1n01^n0, followed by the n2n^2 adjacency-matrix
    12bits in row order, followed by 1k01^k0. Polynomial running time is measured
    13in the length of this word.
    14-/
    15
    16namespace Lax222097.GraphEncoding
    17
    18open scoped Classical
    19
    20open List Turing Lax434930.PolynomialTime
    21
    22/-- An input graph together with the requested solution-size threshold. -/
    23structure Instance where
    24 /-- The number of vertices. -/
    25 order : ℕ
    26 /-- A simple graph on vertices numbered from zero to `order - 1`. -/
    27 graph : SimpleGraph (Fin order)
    28 /-- The requested lower bound on the size of a solution. -/
    29 threshold : ℕ
    30
    31/-- Encode a natural number as that many one-bits followed by a zero-bit. -/
    32def unary (n : ℕ) : Word := replicate n true ++ [false]
    33
    34/-- Write the vertex count, the adjacency matrix row by row, and the threshold. -/
    35noncomputable def encode (I : Instance) : Word :=
    36 unary I.order ++
    37 (finRange I.order).flatMap (fun u =>
    38 (finRange I.order).map (fun v => decide (I.graph.Adj u v))) ++
    39 unary I.threshold
    40
    41/-- The instance transformation can be computed in polynomial time on these binary encodings. -/
    42def PolynomialTime (f : Instance → Instance) : Prop :=
    43 Nonempty (TM2ComputableInPolyTime encode encode f)
    44
    45end Lax222097.GraphEncoding
    46
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…