Fix #1099: KColoring to Satisfiability

[isPANN]

Summary

Add a direct, witness-preserving CNF encoding from runtime K-Coloring on simple graphs to Satisfiability.

Fixes#1099

[codecov]

Codecov Report

❌ Patch coverage is 97.67198% with 111 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.94%. Comparing base (cb54ea0) to head (cc67770).

Files with missing lines	Patch %	Lines
src/rules/graph.rs	94.81%	29 Missing ⚠️
src/unit_tests/growth.rs	96.01%	25 Missing ⚠️
src/unit_tests/rules/pareto.rs	98.22%	22 Missing ⚠️
src/growth.rs	98.22%	11 Missing ⚠️
src/solvers/registry.rs	95.73%	9 Missing ⚠️
src/solvers/ilp/solver.rs	86.20%	4 Missing ⚠️
src/rules/pareto.rs	97.95%	3 Missing ⚠️
src/unit_tests/solvers/brute_force.rs	83.33%	3 Missing ⚠️
src/unit_tests/solvers/registry.rs	98.70%	3 Missing ⚠️
src/solvers/resolver.rs	98.71%	1 Missing ⚠️
... and 1 more

Additional details and impacted files

@@ Coverage Diff @@## main #1108 +/- ##
==========================================
- Coverage 98.00% 97.94% -0.07% 
==========================================
Files 1044 1053 +9 Lines 107366 110791 +3425 ==========================================
+ Hits 105228 108513 +3285 - Misses 2138 2278 +140 

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[isPANN]

Implementation Summary

Changes

• Added a direct KColoring<KN, SimpleGraph> to Satisfiability reduction using one-hot assignment variables, pairwise exactly-one clauses, and edge-conflict clauses.
• Added exact reduction overhead metadata, witness extraction, and the canonical five-cycle example.
• Added ten focused tests covering the closed loop, clause structure and sizes, extraction, feasible and infeasible cycles, zero-color cases, disconnected and isolated vertices, self-loops, parallel edges, and more colors than vertices.
• Added the fixture-driven paper theorem and tutorial plus the SAT 2024 primary-source citation.
• Regenerated and verified graph, schema, and canonical-example exports; ignored generated outputs were not committed.

Verification

• Mathematical constructor: 739,171 checks, 0 failures.
• Independent adversary: 52,533 checks, 0 failures.
• Cross-comparison: 8,605 instances, 0 disagreements.
• Full workspace tests, documentation tests, paper build, formatting, and clippy all passed.

Deviations from Plan

• None.

Open Questions

• None.

[isPANN]

Agentic Review Report

Review base:a9067297 (1075-growth-domain)

Structural Check

Structural Review: rule KColoring → Satisfiability

Structural Completeness

#	Check	Status
1	Rule file exists	PASS — src/rules/kcoloring_satisfiability.rs
2	#[reduction(...)] macro present	PASS — src/rules/kcoloring_satisfiability.rs:39
3	ReductionResult impl present	PASS — src/rules/kcoloring_satisfiability.rs:18
4	ReduceTo impl present	PASS — src/rules/kcoloring_satisfiability.rs:46
5	Test link present	PASS — src/rules/kcoloring_satisfiability.rs:110
6	Test file exists	PASS — src/unit_tests/rules/kcoloring_satisfiability.rs
7	Closed-loop test present	PASS — src/unit_tests/rules/kcoloring_satisfiability.rs:11
8	Registered in rules/mod.rs	PASS — module at src/rules/mod.rs:56; example aggregation at src/rules/mod.rs:468
9	Canonical rule example registered	PASS — C5/k=3 fixture and source/target witnesses at src/rules/kcoloring_satisfiability.rs:91
10	Example-db lookup tests exist	PASS — generic lookup/build and authored-direct-reduction coverage; full consistency suite passed
11	Paper reduction-rule entry	PASS — docs/paper/reductions.typ:12200
12	Blacklisted generated files absent	PASS — none appears in the corrected five-file diff

Build Status

• make test: PASS — 5,441 library tests, 75 integration tests, 330 CLI tests, 17 pred_sym tests, 26 macro tests, and all doctests passed
• make clippy: PASS — all targets with ilp-highs, warnings denied

Semantic Review

• PR scope: OK — against a9067297, exactly five task-specific files and 374 insertions.
• Reduction construction: OK — the variable map and ALO, AMO, and edge-conflict clauses exactly match the issue.
• Mathematical trace: OK — the two-vertex, one-edge, three-color trace produces the expected six variables, two ALO clauses, six AMO clauses, and three edge-conflict clauses.
• extract_solution: OK — partitions the assignment into vertex blocks and returns the unique true color.
• Overhead accuracy: OK — nk variables, n+n*k*(k-1)/2+mk clauses, and nk+n*k*(k-1)+2mk literals match construction and paper.
• Canonical example: OK — C5/k=3 witness and 15-bit assignment match; C5/k=2 infeasibility is tested.
• Edge cases: OK — empty/k=0, nonempty/k=0, loops, parallel edges, disconnected/isolated vertices, and k>n are covered.
• Paper proof and literature: OK — both correctness directions, extraction, exact counts, domain extensions, and SAT 2024 citation are sound.
• Primitive registration: OK — exactly one primitive endpoint implementation exists.

Issue Compliance

#	Check	Status
1	Source/target match	OK
2	Reduction algorithm matches	OK
3	Solution extraction matches	OK
4	Correctness preserved	OK
5	Overhead expressions match	OK
6	Example matches	OK

Summary

• 12/12 structural checks passed
• 6/6 issue-compliance checks passed
• No structural or semantic issues found

---

Quality Check

Quality Review

Design Principles

• DRY: OK — variable indexing is centralized and encoding/extraction logic is not duplicated.
• KISS: OK — the three CNF clause families use direct loops without unnecessary abstractions.
• HC/LC: OK — construction, extraction, example, registration, documentation, and tests remain in their appropriate modules.

HCI

• Not applicable — no CLI or MCP files changed in the corrected review range.

Test Quality

• Naive test detection: OK
  • Nontrivial five-vertex closed loop verifies extracted witnesses.
  • Exact variable, clause, literal, and clause-family assertions independently pin down the encoding.
  • Feasible and infeasible odd-cycle cases test both directions.
  • Boundary/adversarial coverage includes zero colors, empty/disconnected graphs, loops, parallel edges, and excess colors.
  • Extraction is checked against a concrete satisfying assignment.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

None.

Minor (Nice to Have)

None.

Summary

• No quality issues found.
• The five-file change is focused, direct, cohesive, and supported by substantive semantic and edge-case tests.

---

Agentic Feature Tests

Feature:KColoring/SimpleGraph/KN → Satisfiability
Mode: Blind documentation review followed by verification against PR head cc67770a
Verdict: Pass
Critical issues: 0

Documentation Surface

• README.md
• docs/src/cli.md

The documented catalog workflow makes the direct rule discoverable without source inspection.

Verification Results

Check	Command	Result
Catalog registration	pred list | rg 'KColoring|Satisfiability'	PASS — source and target variants listed
Source details/rule discovery	pred show KColoring	PASS — direct Satisfiability edge and overhead displayed
Target details	pred show Satisfiability	PASS — fields and incoming KColoring edge displayed
Canonical source creation	pred create --example KColoring/SimpleGraph/KN --to Satisfiability	PASS — canonical C5/k=3 created
Source solve	pred solve kcoloring.json --solver brute-force	PASS — Or(true), coloring [0,1,0,1,2]
Direct reduction	pred reduce kcoloring.json --to Satisfiability	PASS — one-step path, 15 variables, 35 clauses
Bundle solve/extraction	pred solve kcoloring-to-sat.json --solver brute-force	PASS — extracted [2,1,2,1,0]
Extracted witness evaluation	pred evaluate kcoloring.json --config 2,1,2,1,0	PASS — Or(true)

Findings

No functional, discoverability-blocking, or documentation-blocking issues were found. The direct rule is discoverable, creates the expected target, solves through the bundle, and extracts a valid coloring. No tracked files were modified.

---

Generated by review-pipeline