Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.graph-coloring

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/graph_coloring.clj1 definitions, 3 theorems

AHoF Greedy Graph Coloring: assign colors to vertices so no edge joins two of the same color, using few colors -- the model for register allocation, exam scheduling, and frequency assignment. The greedy heuristic visits vertices in some order and gives each the smallest color not used by an already-colored neighbor. The core check is the edge CONFLICT: two adjacent vertices conflict exactly when they share a color, conflict? color-a color-b = (color-a <= color-b) AND (color-b <= color-a) (the colors are equal), over exact-rational (integer) colors. Proved native and axiom-free: the conflict test as color equality (a boolean conjunction of two comparisons via logic/if-data); that equal colors on adjacent vertices conflict (that color is forbidden); the certificates that a conflict's colors coincide (each at most the other, native nnrat/at-most); and that different colors are conflict-free (a proper coloring of that edge). The neighbor scan and smallest- available-color choice are executable; what is proved is the edge-conflict decision. Requires audit/decide-nnrat-at-most, logic/if-data, nnrat/at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.graph-coloring` prints this classification.

graph-coloring/conflict? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

graph-coloring/same-color-conflicts :
  → floyd-cycle/meet? 2 2 = data/true

graph-coloring/conflict-colors-coincide :
  → 2 ≤ 2

graph-coloring/different-colors-proper :
  → floyd-cycle/meet? 2 5 = data/false