Documentation

DescriptiveComplexity.Problems.TwoSat.Implication

The implication graph of a width-two CNF #

The criterion for 2-satisfiability (Aspvall, Plass & Tarjan 1979) in the form the PTIME membership of 2SAT needs: a width-two CNF with no empty clause is satisfiable iff no variable reaches its own negation and back in the implication graph.

The criterion itself is proved once and for all, without any logic, in DescriptiveComplexity.TwoCnf: it is about an arbitrary 2-CNF, given as a relation on literals over a finite type of variables. This file is its instance for CNF structures: the variables are the elements of the universe, and the clauses are the pairs of occurrences that cover a clause of the structure (DescriptiveComplexity.TwoSatImpl.clauseRel, using DescriptiveComplexity.exists_covering_pair for the width promise). A clause covered by (x, s) and (y, u) is the disjunction ℓ(x, s) ∨ ℓ(y, u), hence the two implications ¬ℓ(x, s) → ℓ(y, u) and ¬ℓ(y, u) → ℓ(x, s); a unit clause is the case (y, u) = (x, s), whose implication ¬ℓ(x, s) → ℓ(x, s) forces the literal, so it needs no separate treatment.

What the instance has to supply is the dictionary in both directions between satisfying the structure (some occurrence of every clause is true) and satisfying the abstract 2-CNF (some literal of every clause is true), which is where the width promise and the absence of an empty clause are used.

The implication graph of a CNF structure #

source
def DescriptiveComplexity.TwoSatImpl.Covers {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) (s : Bool) (y : A) (u : Bool) :
Prop

The clause c is covered by the two signed occurrences (x, s) and (y, u): both occur in it, and nothing else does.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.TwoSatImpl.Step {A : Type} [FirstOrder.Language.sat.Structure A] (p q : A × Bool) :
    Prop

    One step of the implication graph: a clause covered by (x, s) and (y, u) implies ¬ℓ(x, s) → ℓ(y, u) and ¬ℓ(y, u) → ℓ(x, s).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      @[reducible, inline]
      abbrev DescriptiveComplexity.TwoSatImpl.Reach {A : Type} [FirstOrder.Language.sat.Structure A] :
      A × Bool → A × Bool → Prop

      Reachability in the implication graph.

      Equations
      Instances For
        Dependency graph

        Reading the structure as an abstract 2-CNF #

        source
        def DescriptiveComplexity.TwoSatImpl.clauseRel (A : Type) [FirstOrder.Language.sat.Structure A] (p q : A × Bool) :
        Prop

        The structure read as a 2-CNF in the sense of DescriptiveComplexity.TwoCnf: the variables are the elements, and p ∨ q is a clause when some clause of the structure is covered by the occurrences p and q.

        Equations
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.TwoSatImpl.step_iff {A : Type} [FirstOrder.Language.sat.Structure A] (p q : A × Bool) :
          Step p q ↔ TwoCnf.Step (clauseRel A) p q
          Dependency graph
          source
          theorem DescriptiveComplexity.TwoSatImpl.reach_iff {A : Type} [FirstOrder.Language.sat.Structure A] (p q : A × Bool) :
          Reach p q ↔ TwoCnf.Reach (clauseRel A) p q
          Dependency graph
          source
          theorem DescriptiveComplexity.TwoSatImpl.satisfies_of_satClauses {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (hν : ∀ (c : A), SatOcc.IsCl c → ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) :
          TwoCnf.Satisfies (clauseRel A) ν

          A satisfying assignment of the structure satisfies the abstract 2-CNF.

          Dependency graph
          source
          theorem DescriptiveComplexity.TwoSatImpl.satisfiable_of_satisfies {A : Type} [FirstOrder.Language.sat.Structure A] (hw : WidthAtMostTwo A) (hempty : ∀ (c : A), ¬SatOcc.EmptyCl c) {ν : A → Prop} (h : TwoCnf.Satisfies (clauseRel A) ν) :
          Satisfiable A

          Conversely, an assignment satisfying the abstract 2-CNF satisfies the structure – provided the width promise holds and no clause is empty, which is what makes every clause the disjunction of a covering pair.

          Dependency graph

          The criterion, for CNF structures #

          source
          theorem DescriptiveComplexity.TwoSatImpl.no_bad_cycle_of_satisfiable {A : Type} [FirstOrder.Language.sat.Structure A] (h : Satisfiable A) (x : A) (s : Bool) :
          ¬(Reach (x, s) (x, !s) ∧ Reach (x, !s) (x, s))

          No satisfiable instance has a bad cycle: a variable reaching its own negation and back would be both true and false.

          Dependency graph
          source
          theorem DescriptiveComplexity.TwoSatImpl.satisfiable_of_no_bad_cycle {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] (hw : WidthAtMostTwo A) (hempty : ∀ (c : A), ¬SatOcc.EmptyCl c) (hcyc : ∀ (x : A) (s : Bool), ¬(Reach (x, s) (x, !s) ∧ Reach (x, !s) (x, s))) :
          Satisfiable A

          The criterion for 2-satisfiability: a width-two CNF with no empty clause and no variable reaching its own negation and back is satisfiable. This is DescriptiveComplexity.TwoCnf.exists_satisfies_of_no_bad_cycle read through the dictionary above.

          Dependency graph