Lax Lean Archive

Binary encoding of graph decision instances

Lax762056.GraphEncoding · concepts/Lax762056/GraphEncoding.lean · lax-762056

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 Lax762056.GraphEncoding
    17
    18open List Turing Lax434930.PolynomialTime
    19
    20structure Instance where
    21 order : ℕ
    22 graph : SimpleGraph (Fin order)
    23 threshold : ℕ
    24
    25def unary (n : ℕ) : Word := replicate n true ++ [false]
    26
    27noncomputable def encode (I : Instance) : Word := by
    28 classical
    29 exact unary I.order ++
    30 (finRange I.order).flatMap (fun u =>
    31 (finRange I.order).map (fun v => decide (I.graph.Adj u v))) ++
    32 unary I.threshold
    33
    34def PolynomialTime (f : Instance → Instance) : Prop :=
    35 Nonempty (TM2ComputableInPolyTime encode encode f)
    36
    37end Lax762056.GraphEncoding
    38
    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…