Lax Lean Archive

Binary encoding of CNF formulas

Lax429075.Encoding · concepts/Lax429075/Encoding.lean · lax-429075

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

    Lists use a one-bit continuation marker and a zero-bit terminator. A literal consists of its variable index in unary, a zero terminator, and its sign. This encoding gives every formula a unique binary word and bounds each variable index by the word length.

    Concept map
    3 concepts; 16 descendants hidden
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 1 of this submission's paper

    Lean source view on GitHub

    1import Lax429075.CNF
    2
    3/-!
    4---
    5title: Binary encoding of CNF formulas
    6type: definition
    7---
    8Lists use a one-bit continuation marker and a zero-bit terminator.
    9A literal consists of its variable index in unary, a zero terminator, and
    10its sign. This encoding gives every formula a unique binary word and bounds
    11each variable index by the word length.
    12-/
    13
    14namespace Lax429075.Encoding
    15
    16open CNF Lax434930.PolynomialTime
    17
    18def encodeList {α : Type} (encode : α → Word) : List α → Word
    19 | [] => [false]
    20 | a :: as => true :: (encode a ++ encodeList encode as)
    21
    22def encodeNat (n : ℕ) : Word := List.replicate n true ++ [false]
    23
    24def encodeLiteral (l : Literal) : Word := encodeNat l.index ++ [l.positive]
    25
    26def encodeClause : Clause → Word := encodeList encodeLiteral
    27
    28def encodeCNF : Formula → Word := encodeList encodeClause
    29
    30def parseNat : Word → Option (ℕ × Word)
    31 | [] => none
    32 | false :: w => some (0, w)
    33 | true :: w => do
    34 let (n, rest) ← parseNat w
    35 pure (n + 1, rest)
    36
    37def parseLiteral (w : Word) : Option (Literal × Word) := do
    38 let (n, rest) ← parseNat w
    39 match rest with
    40 | [] => none
    41 | sign :: tail => pure (⟨n, sign⟩, tail)
    42
    43def parseList {α : Type} (parse : Word → Option (α × Word)) :
    44 ℕ → Word → Option (List α × Word)
    45 | 0, _ => none
    46 | _ + 1, [] => none
    47 | _ + 1, false :: w => some ([], w)
    48 | fuel + 1, true :: w => do
    49 let (a, rest) ← parse w
    50 let (as, tail) ← parseList parse fuel rest
    51 pure (a :: as, tail)
    52
    53def parseClause (w : Word) : Option (Clause × Word) := parseList parseLiteral w.length w
    54
    55def decodeCNF (w : Word) : Option Formula := do
    56 let (F, rest) ← parseList parseClause w.length w
    57 if rest = [] then pure F else none
    58
    59end Lax429075.Encoding
    60
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…