The order-free first-order interpretation from SAT to independent set

The reductions in this module use order-free first-order interpretations. Input structures have no built-in order or numeric predicates; these are variants of the standard ordered setting.

The complement of Karp's SAT-to-clique occurrence graph [Kar72] gives an order-free interpretation from satisfiability to independent set on CNF structures of at least two elements (Cslib.Logic.FO.cnf.reducesNontrivial_SAT_IndependentSet). The graph has a vertex for each occurrence of a literal in a clause; two occurrences in the same clause are adjacent, and so are two occurrences of complementary literals. An independent set with one vertex per clause picks a literal of each clause, consistently, so it exists exactly when the formula is satisfiable. The target size, a relation of the vocabulary sizedGraph, is given by one extra vertex per clause, adjacent to every vertex; on a structure with at least two clauses no independent set of the target size contains one. Clauses of any width are handled, so no reduction to 3SAT is needed.

The reduction is not correct on all finite structures: every sizedGraph structure with at most one element has an independent set of its target size, and an interpretation maps a structure with one element to a structure with at most one element, while the empty clause on one element is an unsatisfiable CNF structure. So SAT is not order-free reducible to independent set in the sense of Cslib.Logic.FO.Reduces; the reduction is one on nontrivial structures (Cslib.Logic.FO.ReducesNontrivial). Hardness consequences for existential second-order definable classes remain a separate development; definability of the target classes is proved in Complexity.Logics.SecondOrder.IndependentSet.

Main definitions

• Cslib.Logic.FO.cnf.independentSetInterpretation: the occurrence graph, a tagged interpretation.

Main results

• Cslib.Logic.FO.sizedGraph.copyInvariant_IndependentSet: independent set is invariant under copies.
• Cslib.Logic.FO.sizedGraph.mem_IndependentSet_of_subsingleton: structures with at most one element are instances with a solution.
• Cslib.Logic.FO.cnf.mem_independentSet_iff_satisfiable: on a CNF structure with at least two elements, the occurrence graph has an independent set of the target size exactly when the structure is satisfiable.
• Cslib.Logic.FO.cnf.not_reduces_SAT_IndependentSet: the singleton obstruction to an unrestricted order-free reduction.
• Cslib.Logic.FO.cnf.reducesNontrivial_SAT_IndependentSet: SAT reduces to independent set on nontrivial structures.

References

• R. M. Karp, Reducibility among combinatorial problems
• M. R. Garey and D. S. Johnson, Computers and Intractability
• N. Immerman, Descriptive Complexity

Independent sets of copies and of small structures

theorem Cslib.Logic.FO.sizedGraph.mem_IndependentSet_of_subsingleton {M : Type w} [sizedGraph.Structure M] [Subsingleton M] : CategoryTheory.Bundled.of M ∈ IndependentSet

Every structure with at most one element has an independent set of the requested size.

theorem Cslib.Logic.FO.sizedGraph.copyInvariant_IndependentSet : CopyInvariant IndependentSet

Independent set is invariant under any finite positive number of disjoint copies.

The occurrence graph

theorem Cslib.Logic.FO.cnf.not_reduces_SAT_IndependentSet : ¬Reduces SAT sizedGraph.IndependentSet

No order-free first-order interpretation reduces SAT to independent set on all finite structures: a singleton empty clause is unsatisfiable, but every interpreted singleton is an independent-set yes-instance.

inductive Cslib.Logic.FO.cnf.OccurrenceTag : Type

The kinds of vertices of the occurrence graph: the occurrences of literals of each polarity, and the vertices of the target size.

• occ (b : Bool) : OccurrenceTag

  The occurrences of literals of polarity b.

• sizeV : OccurrenceTag

  The vertices counting the clauses.

def Cslib.Logic.FO.cnf.instDecidableEqOccurrenceTag.decEq (x✝ x✝¹ : OccurrenceTag) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Logic.FO.cnf.instDecidableEqOccurrenceTag : DecidableEq OccurrenceTag

instance Cslib.Logic.FO.cnf.instFiniteOccurrenceTag : Finite OccurrenceTag

@[reducible, inline]

abbrev Cslib.Logic.FO.cnf.OccurrenceTag.Coord : OccurrenceTag → Type

The coordinates of the vertices: the clause and the variable of an occurrence, and the clause of a size vertex.

instance Cslib.Logic.FO.cnf.instFiniteOccurrenceTagCoord (t : OccurrenceTag) : Finite t.Coord

def Cslib.Logic.FO.cnf.occurrenceEdges (t : OccurrenceTag) : List (TaggedInterpretation.Template cnf OccurrenceTag.Coord t)

The edges from each kind of vertex: an occurrence is joined to the occurrences in its clause and to the occurrences of the complementary literal, and a size vertex to every vertex.

noncomputable def Cslib.Logic.FO.cnf.occurrenceAdj (t w : OccurrenceTag) : cnf.Formula (t.Coord ⊕ w.Coord)

The formula of the edges between vertices of kinds t and w.

noncomputable def Cslib.Logic.FO.cnf.independentSetInterpretation : TaggedInterpretation cnf sizedGraph OccurrenceTag OccurrenceTag.Coord

The occurrence graph of a CNF structure, with the size vertices as target size.

theorem Cslib.Logic.FO.cnf.mem_independentSet_iff_satisfiable {M : Type w} [cnf.Structure M] [Finite M] [Nontrivial M] : CategoryTheory.Bundled.of (independentSetInterpretation.Model M) ∈ sizedGraph.IndependentSet ↔ Satisfiable M

Correctness of the occurrence graph: on a CNF structure with two distinct elements, the occurrence graph has an independent set of the target size exactly when the structure is satisfiable.

theorem Cslib.Logic.FO.cnf.reducesNontrivial_SAT_IndependentSet : ReducesNontrivial SAT sizedGraph.IndependentSet

SAT reduces to independent set by an order-free interpretation on nontrivial structures, using Karp's occurrence graph [Kar72].