Degrees of CNF incidence vertices

Degrees count listed literal incidences, including repeated literals within one clause. This is the degree convention required by the canonical three-port drawing construction.

Main results

• Cslib.Complexity.SAT.count_incidenceGraph_variable: variable degree is its literal count.
• Cslib.Complexity.SAT.count_incidenceGraph_clause: clause degree is its length.
• Cslib.Complexity.SAT.incidenceGraph_degree_le: width and occurrence bounds bound all degrees.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3

theorem Cslib.Complexity.SAT.count_incidenceGraph_variable {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) {v : V} (hv : v ∈ φ.vars) : List.count (List.idxOf v φ.distinctVars) (incidenceGraph φ).incidenceVertices = List.count v φ.vars

A variable's graph degree counts every occurrence, including repetitions within one clause.

theorem Cslib.Complexity.SAT.count_incidenceGraph_clause {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) (i : ℕ) : List.count (φ.distinctVars.length + i) (incidenceGraph φ).incidenceVertices = List.length (List.getD φ i [])

A clause vertex has one incidence for every literal position; an out-of-range clause has no incidences.

theorem Cslib.Complexity.SAT.incidenceGraph_degree_le {V : Type} [DecidableEq V] {φ : Logic.PL.CNF V} {k : ℕ} (hw : ∀ c ∈ φ, List.length c ≤ k) (hv : ∀ (v : V), List.count v φ.vars ≤ k) (v : ℕ) : List.count v (incidenceGraph φ).incidenceVertices ≤ k

Width and literal-occurrence bounds give the actual listed-incidence degree bound needed by canonical ports. Parallel edge records are counted separately.