Lax Lean Archive

Conjunctive normal form

Lax429075.CNF · concepts/Lax429075/CNF.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

    A literal names a natural-number variable and its sign. A CNF formula is a list of clauses, each a list of literals. Empty clauses are false and the empty conjunction is true. Satisfiability quantifies over Boolean assignments.

    Concept map
    2 concepts; 22 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 Lax434930.PolynomialTime
    2
    3/-!
    4---
    5title: Conjunctive normal form
    6type: definition
    7---
    8A literal names a natural-number variable and its sign. A CNF formula is a
    9list of clauses, each a list of literals. Empty clauses are false and the
    10empty conjunction is true. Satisfiability quantifies over Boolean assignments.
    11-/
    12
    13namespace Lax429075.CNF
    14
    15structure Literal where
    16 index : ℕ
    17 positive : Bool
    18 deriving DecidableEq
    19
    20abbrev Clause := List Literal
    21abbrev Formula := List Clause
    22abbrev Assignment := ℕ → Bool
    23
    24def Literal.eval (l : Literal) (ρ : Assignment) : Bool :=
    25 if l.positive then ρ l.index else !(ρ l.index)
    26
    27def eval (F : Formula) (ρ : Assignment) : Bool :=
    28 F.all fun C => C.any fun l => l.eval ρ
    29
    30def Satisfiable (F : Formula) : Prop := ∃ ρ, eval F ρ = true
    31
    32end Lax429075.CNF
    33
    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…