Lax Lean Archive

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

The Implication Graph of a 2-CNF Formula

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

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

    The implication graph of a 2-CNF formula is the directed graph on the literals in which a clause (a∨b)(a \lor b) contributes the two edges ¬a→b\lnot a \to b and ¬b→a\lnot b \to a, and a unit clause (a)(a) the edge ¬a→a\lnot a \to a. An edge u→vu \to v says that any assignment making uu true must make vv true, and so does a path. A variable xx is contradictory when xx reaches ¬x\lnot x and ¬x\lnot x reaches xx.

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

    Lean source view on GitHub

    1import Lax117284.TwoSatCNF
    2import Mathlib.Logic.Relation
    3
    4/-!
    5---
    6title: The Implication Graph of a 2-CNF Formula
    7type: definition
    8---
    9The implication graph of a 2-CNF formula is the directed graph on the literals in which a
    10clause (a∨b)(a \lor b) contributes the two edges ¬a→b\lnot a \to b and ¬b→a\lnot b \to a, and a unit
    11clause (a)(a) the edge ¬a→a\lnot a \to a. An edge u→vu \to v says that any assignment making uu true
    12must make vv true, and so does a path. A variable xx is *contradictory* when xx reaches
    13¬x\lnot x and ¬x\lnot x reaches xx.
    14
    15# Formalization Notes
    16
    17The graph is a relation on all literals, with no vertex set: a literal that no clause mentions
    18has no edges, and reachability is the reflexive-transitive closure of the edge relation. The
    19algorithm restricts its attention to the literals whose index is below a bound; that is its
    20business, and the criterion is stated for the graph as a whole.
    21
    22The edge relation is written by the shape of the clause. A clause of one literal bb gives
    23¬b→b\lnot b \to b; a clause [a′,b][a', b] gives ¬a′→b\lnot a' \to b and, read from the other end,
    24¬b→a′\lnot b \to a'. A clause with two copies of the same literal gives one edge twice, and a
    25clause with more than two literals gives no edge at all, since the graph is only meant for
    26formulas in 2-CNF.
    27-/
    28
    29namespace Lax117284.TwoSatImplicationGraph
    30
    31open Lax429075.CNF
    32
    33/-- The negation of a literal: the same variable, the opposite sign. -/
    34def negate (l : Literal) : Literal := ⟨l.index, !l.positive⟩
    35
    36/-- The positive literal of the variable `x`. -/
    37def pos (x : ℕ) : Literal := ⟨x, true⟩
    38
    39/-- The negative literal of the variable `x`. -/
    40def neg (x : ℕ) : Literal := ⟨x, false⟩
    41
    42/-- **The edges of the implication graph**: `a → b` when some clause is `[b]` with `a = ¬b`, or
    43some clause is `[¬a, b]` or `[b, ¬a]`. -/
    44def Implies (F : Formula) (a b : Literal) : Prop :=
    45 ∃ C ∈ F, (C = [b] ∧ a = negate b) ∨ C = [negate a, b] ∨ C = [b, negate a]
    46
    47/-- **Reachability** in the implication graph, by a path of any length including zero. -/
    48def Reaches (F : Formula) : Literal → Literal → Prop := Relation.ReflTransGen (Implies F)
    49
    50/-- **A contradictory variable**: it reaches its negation, and its negation reaches it. -/
    51def Contradictory (F : Formula) (x : ℕ) : Prop :=
    52 Reaches F (pos x) (neg x) ∧ Reaches F (neg x) (pos x)
    53
    54end Lax117284.TwoSatImplicationGraph
    55
    Formalization Notes

    The graph is a relation on all literals, with no vertex set: a literal that no clause mentions has no edges, and reachability is the reflexive-transitive closure of the edge relation. The algorithm restricts its attention to the literals whose index is below a bound; that is its business, and the criterion is stated for the graph as a whole.

    The edge relation is written by the shape of the clause. A clause of one literal bb gives ¬b→b\lnot b \to b; a clause [a′,b][a', b] gives ¬a′→b\lnot a' \to b and, read from the other end, ¬b→a′\lnot b \to a'. A clause with two copies of the same literal gives one edge twice, and a clause with more than two literals gives no edge at all, since the graph is only meant for formulas in 2-CNF.

    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…