Corpus: the pigeonhole and graph-coloring families are the same formula — 4 instances provide 2 instances of coverage

[InauguralPhysicist]

What

Two pairs in tests/corpus/manifest.txt are declared as different families but are byte-identical formulas once clauses are normalized (sort literals within a clause, sort clauses, drop comments):

A	B	declared families	clause sets
pigeonhole-4-3-unsat	k4-3color-unsat	pigeonhole vs graph-coloring	identical (12 vars, 34 clauses)
satlib-style-pigeonhole-5-4	satlib-style-k5-4color	vendored-pigeonhole vs vendored-graph-coloring	identical (20 vars, 75 clauses)

They only differ in their c comment headers.

Reproduce:

norm() { grep -vE '^\s*(c|p|$)' "$1" | tr -s ' ' | sed 's/ 0$//;s/^ //' \
  | while read -r l; do echo "$l" | tr ' ' '\n' | sort -n | tr '\n' ' '; echo; done | sort; }
diff <(norm tests/corpus/vendor/satlib_style_pigeonhole_5_4.cnf) \
     <(norm tests/corpus/vendor/satlib_style_k5_4color.cnf) && echo IDENTICAL
diff <(norm tests/corpus/pigeonhole_4_3.cnf) \
     <(norm tests/corpus/k4_3color_unsat.cnf) && echo IDENTICAL

The observable symptom in run_smoke.sh is that each pair emits byte-identical solver telemetry — same decisions, propagations, conflicts, learnts, backjumps, heap_pops, clause_allocs, restarts:

corpus cdcl satlib-style-pigeonhole-5-4: family=vendored-pigeonhole   ... decisions=47 propagations=321 conflicts=32 learnts=31 ...
corpus cdcl satlib-style-k5-4color:      family=vendored-graph-coloring ... decisions=47 propagations=321 conflicts=32 learnts=31 ...

This is NOT a solver or loader bug

Proper-coloring a complete graph K_m with n colors is exactly PHP(m, n): every vertex needs ≥1 color, and since all pairs in K_m are adjacent, no two vertices share a color — which is precisely "every pigeon in ≥1 hole, no two pigeons per hole". K5/4-colors ≡ PHP(5,4) and K4/3-colors ≡ PHP(4,3). Both encodings here are the standard ones for their family, so the collision is a genuine mathematical isomorphism, and identical traces are the correct result.

Why it's still worth fixing

The corpus is organized by family to assert breadth of solver coverage. Right now two of those families are the same formula, so the suite reports 4 instances where it exercises 2 distinct search problems — a coverage illusion. A future regression in, say, the graph-coloring path could never be distinguished from the pigeonhole path, and anyone reading the manifest would reasonably assume otherwise.

Suggested fix (either is fine)

1. Break the isomorphism — make the coloring entries non-complete or off-parameter so they stop reducing to PHP: e.g. K5 with 3 colors, a non-complete graph (a cycle or Petersen subgraph), or move pigeonhole to PHP(6,4). This buys genuinely new search behavior.
2. Document it — if the duplication is deliberate (e.g. to pin that two encodings agree), say so in manifest.txt and tests/corpus/vendor/README.md and mark one as an isomorphism check rather than an independent family.

Option 1 is preferable; the corpus is small enough that a redundant instance is a real fraction of it.

Provenance

Found during the ecosystem v0.30.0 → v0.32.0 pin sweep. Not a regression: the telemetry is identical under v0.30.0 and v0.32.0 (full run_smoke.sh logs diff clean modulo timings), and the suite is green on both.

🤖 Generated with Claude Code