Lax Lean Archive

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

#DNF is #P-complete, by one call and by subtraction

Lax859101.DnfComplete · concepts/Lax859101/DnfComplete.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

    Theorem

    #SAT reduces to #DNF by a subtraction: the models of a CNF formula are the assignments of its variables, 2n2^n of them, minus the models of the DNF formula of its negation, as Durand, Hermann, and Kolaitis showed and as Durand, Haak, Kontinen, and Vollmer used for #AC0^0. Hence #DNF is #P-complete under subtractive reductions, and one-call #P-complete, although its support, the satisfiability of a DNF formula, is easy.

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

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

    1 sharpDnf_sharpP_complete proven

    2 sharpDnf_sharpP_oneCallComplete proven

    3 sharpSat_subtractive_sharpDnf 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: #DNF is #P-complete, by one call and by subtraction
    20type: theorem
    21---
    22#SAT reduces to #DNF by a subtraction: the models of a CNF formula are the
    23assignments of its variables, 2n2^n of them, minus the models of the DNF
    24formula of its negation, as Durand, Hermann, and Kolaitis showed and as
    25Durand, Haak, Kontinen, and Vollmer used for #AC0^0. Hence #DNF is
    26#P-complete under subtractive reductions, and one-call #P-complete, although
    27its support, the satisfiability of a DNF formula, is easy.
    28-/
    29
    30namespace Lax859101.DnfComplete
    31
    32open FirstOrder FirstOrder.Language FirstOrder.Language.Structure
    33open Lax904597.Problems Lax904597.Sat Lax799700.SetFamily
    34open Lax366625.CountingProblems Lax366625.CountingClasses Lax366625.WitnessCounting
    35 Lax366625.CountingSat
    36open Lax859101.OneCallReductions Lax859101.SubtractiveReductions Lax859101.CountingDnf
    37 Lax859101.CountingNaeSat Lax859101.CountingRestrictedSat Lax859101.CountingAllSets
    38 Lax859101.CountingBipartite
    39
    40/-- #SAT reduces to #DNF by a subtractive reduction. -/
    41axiom sharpSat_subtractive_sharpDnf :
    42 SubtractiveReducible SharpSAT SharpDNF
    43
    44/-- #DNF is #P-complete under subtractive reductions. -/
    45axiom sharpDnf_sharpP_complete :
    46 SubtractiveComplete SharpP SharpDNF
    47
    48/-- #DNF is one-call #P-complete. -/
    49axiom sharpDnf_sharpP_oneCallComplete :
    50 OneCallComplete SharpP SharpDNF
    51
    52end Lax859101.DnfComplete
    53
    Show 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…