The finite incidence graph of a CNF formula

Variables receive consecutive names in first-occurrence order. Clause names follow the variable names, with one vertex for each clause position, including repeated and empty clauses. Edges are in literal-occurrence order. Repeated literals therefore give repeated edge records; their incidences remain distinct when drawing routes or bounding degrees.

The representation is the existing binary-encoded Cslib.Complexity.Graph, rather than a new graph type. Natural source variable labels are compared as binary strings and never determine the number of vertices.

Main definitions

• Cslib.Complexity.SAT.incidenceGraph: the variable-clause incidence graph.

Main results

• Cslib.Complexity.SAT.length_vertices_incidenceGraph, Cslib.Complexity.SAT.length_edges_incidenceGraph: exact presentation sizes.
• Cslib.Complexity.SAT.incidenceGraph_endpoints: every edge endpoint is declared.
• Cslib.Complexity.SAT.incidenceGraph_bipartite: each edge joins a variable to a clause.
• Cslib.Complexity.SAT.incidenceGraph_loopless: incidence edges have distinct endpoints.
• Cslib.Complexity.SAT.computableInPolyTime_incidenceGraph: constructing the graph is polynomial-time under binary encodings.

References

This finite-list incidence presentation and its native computation proof are original.

def Cslib.Complexity.SAT.incidenceGraph {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) : Graph

The finite incidence graph, with one edge record for every literal occurrence.

theorem Cslib.Complexity.SAT.length_vertices_incidenceGraph {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) : (incidenceGraph φ).vertices.length = φ.numVars + List.length φ

There is one vertex per distinct variable and per clause position.

theorem Cslib.Complexity.SAT.length_edges_incidenceGraph {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) : (incidenceGraph φ).edges.length = φ.vars.length

Every literal occurrence gives exactly one edge record.

theorem Cslib.Complexity.SAT.incidenceGraph_bipartite {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} {e : ℕ × ℕ} (he : e ∈ (incidenceGraph φ).edges) : e.1 < φ.distinctVars.length ∧ φ.distinctVars.length ≤ e.2 ∧ e.2 < φ.distinctVars.length + List.length φ

The edge records join the variable and clause parts of the declared vertex interval.

theorem Cslib.Complexity.SAT.incidenceGraph_endpoints {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} {e : ℕ × ℕ} (he : e ∈ (incidenceGraph φ).edges) : e.1 ∈ (incidenceGraph φ).vertices ∧ e.2 ∈ (incidenceGraph φ).vertices

Every edge endpoint occurs in the list of declared vertices.

theorem Cslib.Complexity.SAT.incidenceGraph_loopless {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} {e : ℕ × ℕ} (he : e ∈ (incidenceGraph φ).edges) : e.1 ≠ e.2

The variable and clause name intervals are disjoint, so incidence edges are not loops.

theorem Cslib.Complexity.SAT.computableInPolyTime_incidenceGraph {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime incidenceGraph (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) encGraph

Constructing the incidence graph compares binary encodings rather than expanding source variable names to unary.