#2SAT, #HORN-SAT, #Monotone-2SAT, and all the vertex covers of a graph

The model counts of the CNF formulas of a restricted shape: DescriptiveComplexity.SharpTwoSAT (at most two literals per clause), DescriptiveComplexity.SharpHornSAT (at most one positive literal per clause) and DescriptiveComplexity.SharpMonotoneTwoSAT (at most two literals per clause, all positive), each #SAT restricted to a first-order definable class of formulas (DescriptiveComplexity.CountingProblem.restrict), and DescriptiveComplexity.SharpAllVertexCovers, the number of vertex covers of a graph. Deciding the first three is in PTIME; counting their models is one-call #P-complete (Valiant 1979).

The vertex covers of a graph are the complements of its independent sets, so the last problem is counting all the independent sets under another name (DescriptiveComplexity.sharpAllVertexCovers_eq). The three others are reached from it by one reduction with a sign (DescriptiveComplexity.edgeInterp): one clause per edge, holding its two ends as literals of that sign. With the negative sign the models are the independent sets, the formula is a 2-CNF and a Horn formula; with the positive sign the models are the vertex covers, the formula a monotone 2-CNF. In both cases the models are sets of non-isolated vertices, the variables of the formula, and each isolated vertex doubles the count of the graph: the post-processing multiplies by 2 to the number of isolated vertices.

The classes of formulas

noncomputable def DescriptiveComplexity.occS {α : Type} (s : Bool) (c x : α) : FirstOrder.Language.sat.Formula α

The literal (x, s) occurs in the clause c, over the vocabulary of CNF formulas.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.widthTwoS : FirstOrder.Language.sat.Sentence

At most two literals per clause: among any three occurrences of a clause, two coincide.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.hornS : FirstOrder.Language.sat.Sentence

At most one positive literal per clause.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.monotoneS : FirstOrder.Language.sat.Sentence

No negative literal.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.realize_widthTwoS {A : Type} [FirstOrder.Language.sat.Structure A] : A ⊨ widthTwoS ↔ WidthAtMostTwo A

theorem DescriptiveComplexity.realize_hornS {A : Type} [FirstOrder.Language.sat.Structure A] : A ⊨ hornS ↔ AtMostOnePositive A

def DescriptiveComplexity.NoNegative (A : Type) [FirstOrder.Language.sat.Structure A] : Prop

No clause has a negative literal.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.realize_monotoneS {A : Type} [FirstOrder.Language.sat.Structure A] : A ⊨ monotoneS ↔ NoNegative A

The problems

noncomputable def DescriptiveComplexity.SharpTwoSAT : CountingProblem FirstOrder.Language.sat

#2SAT: the number of models of a CNF formula with at most two literals per clause, 0 on the other formulas.

Equations

• DescriptiveComplexity.SharpTwoSAT = DescriptiveComplexity.SharpSAT.restrict DescriptiveComplexity.widthTwoS

noncomputable def DescriptiveComplexity.SharpHornSAT : CountingProblem FirstOrder.Language.sat

#HORN-SAT: the number of models of a Horn formula, 0 on the other formulas.

Equations

• DescriptiveComplexity.SharpHornSAT = DescriptiveComplexity.SharpSAT.restrict DescriptiveComplexity.hornS

noncomputable def DescriptiveComplexity.SharpMonotoneTwoSAT : CountingProblem FirstOrder.Language.sat

#Monotone-2SAT: the number of models of a CNF formula with at most two literals per clause, all positive, 0 on the other formulas.

Equations

• DescriptiveComplexity.SharpMonotoneTwoSAT = DescriptiveComplexity.SharpSAT.restrict (DescriptiveComplexity.widthTwoS ⊓ DescriptiveComplexity.monotoneS)

Graphs: independent sets and vertex covers

def DescriptiveComplexity.GEdge {A : Type} [FirstOrder.Language.graph.Structure A] (x y : A) : Prop

An edge of a graph: two distinct adjacent vertices.

Equations

• DescriptiveComplexity.GEdge x y = (x ≠ y ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y])

def DescriptiveComplexity.NonIso {A : Type} [FirstOrder.Language.graph.Structure A] (x : A) : Prop

A vertex is not isolated: it is an end of an edge.

Equations

• DescriptiveComplexity.NonIso x = ∃ (y : A), DescriptiveComplexity.GEdge x y ∨ DescriptiveComplexity.GEdge y x

def DescriptiveComplexity.GVertexCover (A : Type) [FirstOrder.Language.graph.Structure A] (C : A → Prop) : Prop

A vertex cover: every edge has an end in it.

Equations

• DescriptiveComplexity.GVertexCover A C = ∀ (x y : A), x ≠ y → FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y] → C x ∨ C y

theorem DescriptiveComplexity.card_vertexCover_eq (A : Type) [FirstOrder.Language.graph.Structure A] : Nat.card { C : A → Prop // GVertexCover A C } = Nat.card { S : A → Prop // IndepSet (fun (x y : A) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) S }

The vertex covers are the complements of the independent sets.

noncomputable def DescriptiveComplexity.SharpAllVertexCovers : CountingProblem FirstOrder.Language.graph

Counting all the vertex covers of a graph.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpAllVertexCovers_eq (A : Type) [FirstOrder.Language.graph.Structure A] : SharpAllVertexCovers.Count A = SharpAllIndependentSets.Count A

theorem DescriptiveComplexity.sharpAllVertexCovers_sharpP_oneCallComplete : SharpP.OneCallComplete SharpAllVertexCovers

Counting all the vertex covers of a graph is one-call #P-complete. Registered in the Lax archive as Lax859101.AllSetsComplete.sharpAllVertexCovers_sharpP_oneCallComplete.

One clause per edge

@[reducible, inline]

abbrev DescriptiveComplexity.gAdjOSym : (FirstOrder.Language.graph.sum FirstOrder.Language.order).Relations 2

The adjacency symbol, over the ordered expansion.

Equations

• DescriptiveComplexity.gAdjOSym = Sum.inl FirstOrder.Language.adj

noncomputable def DescriptiveComplexity.edgeDomF : (FirstOrder.Language.graph.sum FirstOrder.Language.order).Formula (Fin 2)

The domain of the clauses: the edges.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.endF : (FirstOrder.Language.graph.sum FirstOrder.Language.order).Formula (Fin 2 × Fin 2)

The variable is an end of the clause.

Equations

• DescriptiveComplexity.endF = (FirstOrder.Language.var (1, 0)).equal (FirstOrder.Language.var (0, 0)) ⊔ (FirstOrder.Language.var (1, 0)).equal (FirstOrder.Language.var (0, 1))

noncomputable def DescriptiveComplexity.edgeInterp (s : Bool) : RelFOInterpretation (FirstOrder.Language.graph.sum FirstOrder.Language.order) FirstOrder.Language.sat Bool 2

One clause per edge, holding its two ends as literals of sign s: the tag true carries the clauses, on the edges, and the tag false the variables, on the diagonal.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.edge_dom_false {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] {s : Bool} (w : Fin 2 → A) : ((edgeInterp s).domFormula false).Realize w ↔ w 0 = w 1

@[reducible, inline]

abbrev DescriptiveComplexity.gAdjSym : FirstOrder.Language.graph.Relations 2

The adjacency symbol.

Equations

• DescriptiveComplexity.gAdjSym = FirstOrder.Language.adj

noncomputable def DescriptiveComplexity.isoF {α : Type} (x : α) : FirstOrder.Language.graph.Formula α

x is isolated.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.isoCount : PolyTerm FirstOrder.Language.graph

The number of isolated vertices, as a polynomial term.

Equations

• DescriptiveComplexity.isoCount = DescriptiveComplexity.PolyTerm.count (FirstOrder.Language.LHom.sumInl.onFormula (DescriptiveComplexity.isoF 0))

theorem DescriptiveComplexity.eval_isoCount {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] : PolyTerm.eval A isoCount = Nat.card { x : A // ¬NonIso x }

theorem DescriptiveComplexity.sharpAllIndependentSets_eq_edge {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] {s : Bool} [Finite A] : SharpAllIndependentSets.Count A = SharpSAT.Count ((edgeInterp s).MapRel A) * 2 ^ Nat.card { x : A // ¬NonIso x }

The count of the graph is the model count of the formula of its edges, doubled for each isolated vertex.

noncomputable def DescriptiveComplexity.sharpAllIndependentSets_oneCall_sharpSat (s : Bool) : OneCallReduction SharpAllIndependentSets SharpSAT

Counting all the independent sets reduces to #SAT with one call, the formula being one clause of sign s per edge.

Equations

• One or more equations did not get rendered due to their size.

What the formula of the edges is

theorem DescriptiveComplexity.edge_widthAtMostTwo {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] {s : Bool} : WidthAtMostTwo ((edgeInterp s).MapRel A)

theorem DescriptiveComplexity.edge_atMostOnePositive {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] : AtMostOnePositive ((edgeInterp false).MapRel A)

theorem DescriptiveComplexity.edge_noNegative {A : Type} [FirstOrder.Language.graph.Structure A] [LinearOrder A] : NoNegative ((edgeInterp true).MapRel A)

Completeness

theorem DescriptiveComplexity.sharpTwoSat_sharpP_oneCallComplete : SharpP.OneCallComplete SharpTwoSAT

#2SAT is one-call #P-complete. Registered in the Lax archive as Lax859101.RestrictedSatComplete.sharpTwoSat_sharpP_oneCallComplete.

theorem DescriptiveComplexity.sharpHornSat_sharpP_oneCallComplete : SharpP.OneCallComplete SharpHornSAT

#HORN-SAT is one-call #P-complete. Registered in the Lax archive as Lax859101.RestrictedSatComplete.sharpHornSat_sharpP_oneCallComplete.

theorem DescriptiveComplexity.sharpMonotoneTwoSat_sharpP_oneCallComplete : SharpP.OneCallComplete SharpMonotoneTwoSAT

#Monotone-2SAT is one-call #P-complete. Registered in the Lax archive as Lax859101.RestrictedSatComplete.sharpMonotoneTwoSat_sharpP_oneCallComplete.