Lax Lean Archive

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

The values of #2SAT, #HORN-SAT, and #Monotone-2SAT

Lax859101.RestrictedSatValues · concepts/Lax859101/RestrictedSatValues.lean · lax-859101

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

    Lemma

    The number counted by each of #2SAT, #HORN-SAT, and #Monotone-2SAT is invariant under isomorphism of instances, so the value of each problem on an instance is the number it counts.

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

    This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.

    1 sharpHornSat_count_iso proven

    2 sharpHornSat_eq proven

    3 sharpMonotoneTwoSat_count_iso proven

    4 sharpMonotoneTwoSat_eq proven

    5 sharpTwoSat_count_iso proven

    6 sharpTwoSat_eq proven

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Sat
    3import Mathlib.ModelTheory.Graph
    4import Lax799700.SetFamily
    5import Lax366625.CountingProblems
    6import Lax366625.CountingClasses
    7import Lax366625.WitnessCounting
    8import Lax366625.CountingSat
    9import Lax859101.OneCallReductions
    10import Lax859101.SubtractiveReductions
    11import Lax859101.CountingDnf
    12import Lax859101.CountingNaeSat
    13import Lax859101.CountingRestrictedSat
    14import Lax859101.CountingAllSets
    15import Lax859101.CountingBipartite
    16
    17/-!
    18---
    19title: The values of #2SAT, #HORN-SAT, and #Monotone-2SAT
    20type: lemma
    21---
    22The number counted by each of #2SAT, #HORN-SAT, and #Monotone-2SAT is
    23invariant under isomorphism of instances, so the value of each problem on an
    24instance is the number it counts.
    25-/
    26
    27namespace Lax859101.RestrictedSatValues
    28
    29open FirstOrder FirstOrder.Language FirstOrder.Language.Structure
    30open Lax904597.Problems Lax904597.Sat Lax799700.SetFamily
    31open Lax366625.CountingProblems Lax366625.CountingClasses Lax366625.WitnessCounting
    32 Lax366625.CountingSat
    33open Lax859101.OneCallReductions Lax859101.SubtractiveReductions Lax859101.CountingDnf
    34 Lax859101.CountingNaeSat Lax859101.CountingRestrictedSat Lax859101.CountingAllSets
    35 Lax859101.CountingBipartite
    36
    37/-- The number counted by #2SAT is isomorphism-invariant. -/
    38axiom sharpTwoSat_count_iso :
    39 ∀ {A B : Type} [Lax904597.Sat.sat.Structure A] [Lax904597.Sat.sat.Structure B],
    40 (A ≃[Lax904597.Sat.sat] B) → Nat.card
    41 {ν : A → Prop // WidthAtMostTwo A ∧ SatModel A ν} = Nat.card
    42 {ν : B → Prop // WidthAtMostTwo B ∧ SatModel B ν}
    43
    44/-- The value of #2SAT is the number it counts. -/
    45axiom sharpTwoSat_eq :
    46 ∀ (A : Type) [Lax904597.Sat.sat.Structure A], SharpTwoSAT A = Nat.card
    47 {ν : A → Prop // WidthAtMostTwo A ∧ SatModel A ν}
    48
    49/-- The number counted by #HORN-SAT is isomorphism-invariant. -/
    50axiom sharpHornSat_count_iso :
    51 ∀ {A B : Type} [Lax904597.Sat.sat.Structure A] [Lax904597.Sat.sat.Structure B],
    52 (A ≃[Lax904597.Sat.sat] B) → Nat.card
    53 {ν : A → Prop // AtMostOnePositive A ∧ SatModel A ν} = Nat.card
    54 {ν : B → Prop // AtMostOnePositive B ∧ SatModel B ν}
    55
    56/-- The value of #HORN-SAT is the number it counts. -/
    57axiom sharpHornSat_eq :
    58 ∀ (A : Type) [Lax904597.Sat.sat.Structure A], SharpHornSAT A = Nat.card
    59 {ν : A → Prop // AtMostOnePositive A ∧ SatModel A ν}
    60
    61/-- The number counted by #Monotone-2SAT is isomorphism-invariant. -/
    62axiom sharpMonotoneTwoSat_count_iso :
    63 ∀ {A B : Type} [Lax904597.Sat.sat.Structure A] [Lax904597.Sat.sat.Structure B],
    64 (A ≃[Lax904597.Sat.sat] B) → Nat.card {ν : A → Prop //
    65 (WidthAtMostTwo A ∧ NoNegative A) ∧ SatModel A ν} = Nat.card {ν : B → Prop //
    66 (WidthAtMostTwo B ∧ NoNegative B) ∧ SatModel B ν}
    67
    68/-- The value of #Monotone-2SAT is the number it counts. -/
    69axiom sharpMonotoneTwoSat_eq :
    70 ∀ (A : Type) [Lax904597.Sat.sat.Structure A], SharpMonotoneTwoSAT A = Nat.card {ν : A → Prop //
    71 (WidthAtMostTwo A ∧ NoNegative A) ∧ SatModel A ν}
    72
    73end Lax859101.RestrictedSatValues
    74
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…