Lax Lean Archive

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

Satisfiability of Horn formulas

Lax535992.HornSat · concepts/Lax535992/HornSat.lean · lax-535992

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

    An instance is a CNF instance of the NP core. It is Horn when every clause has at most one positive literal, and it is a yes-instance of HORN-SAT when it is Horn and satisfiable. HORN-SAT is the decision problem of the structures isomorphic to such an instance. Instances that are not Horn are no-instances: the Horn condition is part of the problem, not a promise.

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

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Semantics
    2import Lax904597.Problems
    3import Lax485149.Problems
    4import Lax904597.Sat
    5
    6/-!
    7---
    8title: Satisfiability of Horn formulas
    9type: definition
    10---
    11An instance is a CNF instance of the NP core. It is Horn when every clause
    12has at most one positive literal, and it is a yes-instance of HORN-SAT when
    13it is Horn and satisfiable. HORN-SAT is the decision problem of the
    14structures isomorphic to such an instance. Instances that are not Horn are
    15no-instances: the Horn condition is part of the problem, not a promise.
    16-/
    17
    18namespace Lax535992.HornSat
    19
    20open Lax904597.Problems Lax485149.Problems
    21
    22open Lax904597.Sat
    23
    24open FirstOrder
    25
    26open Language Structure
    27
    28section HornSat
    29
    30variable (A : Type) [sat.Structure A]
    31
    32/-- Every clause of a CNF instance has at most one positive
    33literal: any two variables occurring positively in the same clause coincide. -/
    34def AtMostOnePositive : Prop :=
    35 ∀ c x y : A, RelMap satIsClause ![c] → RelMap satPosIn ![c, x] →
    36 RelMap satPosIn ![c, y] → x = y
    37
    38/-- A CNF instance is a yes-instance of HORN-SAT if every clause
    39has at most one positive literal and the CNF is satisfiable. -/
    40def HornSatisfiable : Prop :=
    41 AtMostOnePositive A ∧ Satisfiable A
    42
    43end HornSat
    44
    45/-- HORN-SAT: is the CNF instance Horn and satisfiable? -/
    46def HORNSAT : DecisionProblem sat := DecisionProblem.ofPred fun A _ => HornSatisfiable A
    47
    48end Lax535992.HornSat
    49
    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…