Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Correctness of the Algorithm

Lax117284.TwoSatCorrectness · concepts/Lax117284/TwoSatCorrectness.lean · lax-117284

proven

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

    Theorem

    The algorithm accepts a formula exactly when it is in 2-CNF and satisfiable.

    Concept map
    9 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax117284.TwoSatAlgorithm
    2
    3/-!
    4---
    5title: Correctness of the Algorithm
    6type: theorem
    7---
    8The algorithm accepts a formula exactly when it is in 2-CNF and satisfiable.
    9
    10# Formalization Notes
    11
    12The width check accepts exactly the 2-CNF formulas without an empty clause, and the search, by
    13the criterion, rejects exactly the formulas with a contradictory variable. Two points connect
    14the search to the criterion. The set the search computes is the set of literals reachable within
    15the nodes, and reachability in the whole graph from a literal that occurs stays within the
    16nodes, since every edge joins two literals of one clause. And it suffices to test the variables
    17that occur, since a variable that does not occur has no edges at either of its literals and so is
    18never contradictory.
    19-/
    20
    21namespace Lax117284.TwoSatCorrectness
    22
    23open Lax429075.CNF Lax117284.TwoSatCNF Lax117284.TwoSatAlgorithm
    24
    25/-- **The algorithm is correct.** -/
    26axiom decide_iff (F : Formula) : decide F = true ↔ IsTwoCNF F ∧ Satisfiable F
    27
    28end Lax117284.TwoSatCorrectness
    29
    Show Proof
    Formalization Notes

    The width check accepts exactly the 2-CNF formulas without an empty clause, and the search, by the criterion, rejects exactly the formulas with a contradictory variable. Two points connect the search to the criterion. The set the search computes is the set of literals reachable within the nodes, and reachability in the whole graph from a literal that occurs stays within the nodes, since every edge joins two literals of one clause. And it suffices to test the variables that occur, since a variable that does not occur has no edges at either of its literals and so is never contradictory.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…