Fix #1100: SetSplitting to NAESatisfiability

[isPANN]

Summary

Implement the direct witness-preserving reduction from Set Splitting to Not-All-Equal Satisfiability, including verification, tests, canonical example data, and paper documentation.

Fixes #1100

[codecov]

Codecov Report

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

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    #1109      +/-   ##
==========================================
- Coverage   98.00%   97.94%   -0.07%     
==========================================
  Files        1044     1051       +7     
  Lines      107366   110605    +3239     
==========================================
+ Hits       105228   108327    +3099     
- 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 the direct witness-preserving SetSplitting -> NAESatisfiability reduction with deterministic first-occurrence deduplication, positive one-indexed literals, identity extraction, and declared size overhead.
• Added focused closed-loop, structure, duplicate, infeasible, empty-family, unused-variable, and canonical-example tests.
• Registered the rule and canonical example, and documented the construction and proof in the Typst paper.
• Updated the known dominated-rule expectation because the new path makes the existing direct SetSplitting -> ILP edge asymptotically dominated.

Deviations from Plan

• The full test suite exposed the expected new dominated-rule relationship, so its semantic allow-list was updated.
• The PR base was changed from main to 1075-growth-domain, whose tip is the requested starting commit a9067297, keeping the PR scoped to this issue.

Open Questions

• None.

Verification

• Mathematical constructor: 282,166 checks.
• Independent adversary: 347,100 checks.
• Cross-comparison: 6,944 instances / 205,592 assignments, zero disagreements.
• make test, make clippy, make fmt-check, and make paper pass.

[isPANN]

Agentic Review Report

Structural Check

Structural Review: rule SetSplitting → NAESatisfiability

Structural Completeness

#	Check	Status
1	Rule file exists	PASS — src/rules/setsplitting_naesatisfiability.rs
2	#[reduction(...)] macro present	PASS — declares all three target-size overhead fields
3	ReductionResult impl present	PASS
4	ReduceTo<NAESatisfiability> impl present	PASS
5	#[cfg(test)] and test path link present	PASS
6	Test file exists	PASS — src/unit_tests/rules/setsplitting_naesatisfiability.rs
7	Closed-loop test present	PASS — includes the canonical satisfiable instance plus repeated-element and empty-family cases
8	Registered in rules/mod.rs	PASS
9	Canonical rule example registered	PASS — module-local example spec is aggregated by canonical_rule_example_specs()
10	Example-db lookup tests exist	PASS — generic database coverage, uniqueness, and solution-consistency tests pass
11	Paper reduction-rule entry present	PASS
12	Blacklisted generated files absent	PASS — none occur in a9067297..f59e9a9c

Build Status

• make test: PASS — 5,437 library tests, 75 integration tests, 330 CLI tests, 17 symbolic CLI tests, 26 macro tests, and all doctests passed
• make clippy: PASS — cargo clippy --all-targets --features ilp-highs -- -D warnings
• Working tree remained clean after verification

Semantic Review

• Reduction construction: OK — each universe element becomes one variable, and each source subset becomes one positive-literal NAE clause after first-occurrence deduplication.
• Manual trace: OK — subsets [0,1], [1,2,3], and [0,2,3] emit [1,2], [2,3,4], and [1,3,4]; assignment [0,1,0,1] satisfies both representations.
• Duplicate handling: OK — iterator-order filtering through HashSet::insert preserves first occurrence, and removing duplicates cannot change which colors occur.
• Repeated-only subset: OK — [u,u,…] maps to (x_u,x_u), which is NAE-unsatisfiable exactly when the source constraint is unsplittable.
• Empty family and unused elements: OK.
• Solution extraction: OK — source and target dimensions are both universe_size, so identity extraction is correct.
• Correctness preservation: OK — source validity and target NAE validity are pointwise equivalent.
• Overhead accuracy: OK — num_vars = n, num_clauses = m, and literal count sum_j max(2, |D_j|) <= (n+1)m.
• Example quality: OK — complete source/target JSON and a valid identical witness pair.
• Paper statement and proof: OK — construction, both directions, repeated-only NO case, overhead, extraction, and tutorial example are sound.
• Diff scope: OK — exactly five issue-scoped files relative to stacked base a9067297.

Issue Compliance

#	Check	Status
1	Source/target match issue	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 FAIL or ISSUE findings

---

Quality Check

Quality Review

Design Principles

• DRY: OK — concise reduction and identity extraction with no duplicated logic.
• KISS: OK — direct mapping without unnecessary abstraction or branching.
• HC/LC: OK — construction, extraction, registration, tests, and example data remain appropriately localized.

Test Quality

• Naive test detection: ISSUE
  • The sole general closed-loop test uses a satisfiable four-element instance (src/unit_tests/rules/setsplitting_naesatisfiability.rs:7-21), below the review rubric's 5+ variable expectation. The only infeasible case is the special all-repeated-subset encoding (src/unit_tests/rules/setsplitting_naesatisfiability.rs:66-76). There is no ordinary unsatisfiable set family, such as the three two-element subsets of a triangle, or a ≥5-element closed-loop case exercising brute-force equivalence.

Issues

Critical (Must Fix)

None.

Important (Should Fix)

• Add a ≥5-element closed-loop case and a non-degenerate unsatisfiable Set Splitting family to verify satisfiability preservation beyond the canonical happy path.

Minor (Nice to Have)

None.

Summary

• Important — reduction semantics are tested closed-loop only on one satisfiable four-element instance; ordinary infeasibility and a 5+ element instance are missing.

---

Agentic Feature Tests

Feature: SetSplitting → NAESatisfiability
Mode: Blind-style downstream CLI verification, ephemeral profile
Use case: Discover the reduction, create and solve the canonical source instance, reduce it, and solve/evaluate the NAE-SAT result.
Verdict: Pass
Critical issues: 0

Area	Result	Evidence
Discoverability	Pass	pred list includes both models; pred show SetSplitting lists the outgoing rule; pred show NAESatisfiability lists it as incoming.
Canonical source creation	Pass	General and rule-specific pred create --example forms produced valid problem JSON.
Source solving	Pass	Default ILP-path solving and brute force both returned Or(true) with valid splittings.
Reduction	Pass	pred reduce produced an exact SetSplitting → NAESatisfiability bundle.
Target solving	Pass	Bundle solving returned a NAE-SAT witness and correctly extracted the identical source splitting.
Evaluation	Pass	The same assignment evaluated to Or(true) for source and target.
Documentation	Pass	README, CLI guide, and paper commands were sufficient to derive the workflow.

Commands Exercised

pred list
pred show SetSplitting
pred show NAESatisfiability
pred create --example SetSplitting -o set-splitting.json
pred solve set-splitting.json
pred solve set-splitting.json --solver brute-force
pred reduce set-splitting.json --to NAESatisfiability -o bundle.json
pred solve bundle.json
pred create --example SetSplitting --to NAESatisfiability -o rule-source.json
pred reduce rule-source.json --to NAESatisfiability -o rule-bundle.json
pred solve rule-bundle.json --solver brute-force
pred evaluate <source> --config 0,1,0,0,1,1
pred evaluate <target> --config 0,1,0,0,1,1

Findings

No confirmed feature, CLI, or documentation defects. A temporary artifact-directory lock caused by concurrent review jobs was classified as test-environment contention, not a product defect.

---

Generated by review-pipeline