Lax Lean Archive

The satisfiability language and verifier

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

    SAT contains precisely the encodings of satisfiable CNF formulas. A certificate is a finite list of truth values, extended by false outside its length. The verifier accepts a paired formula encoding and certificate when every clause is satisfied. Malformed encodings are outside the language.

    Concept map
    5 concepts; 13 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.Encoding
    2import Lax434930.Certificates
    3
    4/-!
    5---
    6title: The satisfiability language and verifier
    7type: definition
    8---
    9SAT contains precisely the encodings of satisfiable CNF formulas.
    10A certificate is a finite list of truth values, extended by false outside
    11its length. The verifier accepts a paired formula encoding and certificate
    12when every clause is satisfied. Malformed encodings are outside the language.
    13-/
    14
    15namespace Lax429075.Satisfiability
    16
    17open CNF Encoding Lax434930.PolynomialTime Lax434930.Certificates
    18
    19def assignment (y : Word) : Assignment := fun i => (y[i]?).getD false
    20
    21def SAT : Language := {w | ∃ F, encodeCNF F = w ∧ Satisfiable F}
    22
    23def Verifier : Language :=
    24 {z | ∃ (F : Formula) (y : Word), z = pair (encodeCNF F) y ∧ eval F (assignment y) = true}
    25
    26end Lax429075.Satisfiability
    27
    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…