[peda-cos]

Fixes #1100.

Implements the rule: one Boolean variable per universe element, one NAE clause per subset over its distinct elements; a single-distinct-element subset emits the unsatisfiable clause (x_u, x_u). Witnesses extract directly as assignments.

Validated locally: make check passes for the new rule set (6245 lib + example-db suites, >150 dotfiles ok); closed-loop/exhaustive checks per the issue's validation section included.

[peda-cos]

Heads-up: the fork-pull workflow run is stuck at action_required (first contribution needs maintainer approval to execute). Once approved, all 7 CI checks are expected to run; local cargo fmt/clippy/test already pass on this branch.

[GiggleLiu]

Agentic Review Report

Reviewed PR #1195 at 309c562e4f3fe964d47e18fa43dba1086d062369 against merge base 875b6e86d5a87e5f66c2f6743be9d22abe917a09.

Structural and semantic

The clause-per-subset construction is correct on representable ordinary instances, including all-repeated subsets. Module registration, identity aggregate mapping, test linkage, and canonical-example collection exist. The following contract defects block merging.

Quality and findings

1. Critical: the registered clause-variable upper bound is false. src/rules/setsplitting_naesatisfiability.rs:51 declares universe_size * (universe_size + 1), independent of subset count. The accepted source SetSplitting::new(2, vec![vec![0, 1]; 4]) emits four [1, 2] clauses. The target's num_clause_variables() sums distinct variable counts per clause, yielding 8, while the declared bound is 6. This follows directly from the construction and the target getter. Use universe_size * num_subsets and add a repeated-subset regression checking measured parameters.

2. Critical: valid source instances can panic during reduction. At src/rules/setsplitting_naesatisfiability.rs:92, NAESatisfiability::new panics when num_vars > i64::MAX, whereas SetSplitting accepts any usize universe size. On 64-bit targets, SetSplitting::new(usize::MAX, vec![]) allocates no large collections and reaches this panic. Line 74 also casts (element + 1) with as i64. Check the literal-domain boundary, use checked conversion, and call NAESatisfiability::try_new with the typed target-construction error mapping. Add a cheap oversized-empty-universe regression. This is established from the constructor code; a Rust execution probe was not run in this review.

3. Important: required paper theorem is missing. docs/paper/reductions.typ has no reduction-rule("SetSplitting", "NAESatisfiability") entry, and the PR changes only the rule, its test file, and the module collector. Add the directed theorem, construction, proof, and canonical example.

4. Important: planned boundary and rejection coverage is missing. src/unit_tests/rules/setsplitting_naesatisfiability.rs does not test malformed or unsatisfying extraction, empty families, unused universe elements, subsets above arity three, or all-assignment equivalence promised by issue #1100. Add those cases, including the two counterexamples above. The current repeated-member test checks target infeasibility but not the full source/target contract.

Feature test

Not run. No CI checks have executed on this head; the PR discussion says the fork workflow requires maintainer approval. Existing source inspection is enough to establish the two contract defects, so the recommendation is to hold rather than spend the shared build slot on an already failing design.

Verdict

Request changes. The formula and construction error handling need fixes before merging.

GitHub PR audit

GATE: PASS

The harm gate is separate from the correctness verdict.

• harm.secrets: OK. No credential material.
• harm.dangerous-files: OK. Purposeful Rust source and tests only.
• harm.generated-artifacts: OK. No generated exports or build products.
• harm.cache: OK. No cache directories.
• harm.debug-leftovers: OK. No production probes.
• pr.description-quality: ISSUE, advisory. The body claims exhaustive checks, but the committed tests do not contain the promised broad checks; clarify any separate experiment.
• pr.traceable: OK. Links issue #1100 and explains the construction.

[GiggleLiu]

Review fixes

Fixed the SetSplitting → NAE-SAT clause-variable bound to universe_size * num_subsets. Oversized SAT universes now return a typed construction error; validated literal conversion and the fallible target constructor replace unchecked conversion and panic paths.

Added exhaustive pointwise equivalence and extraction checks for 341 small subset families and 4,681 assignments, plus invalid witnesses, repeated subsets, unused elements, empty families, large clauses, measured parameter contracts, and literal-domain boundaries. Added the missing directed theorem, both correctness directions, parameter derivation, and canonical example to the paper.

Validation at 40a445d6162f25995042bd50365f31ff55a92464: independent review passed; make check passed 7,093 tests plus formatting and Clippy; make paper compiled without warnings. The real CLI create → path → reduce → solve flow returned a satisfying NAE witness and extracted a satisfying SetSplitting witness. Only the three intended source/test/paper files changed. Fresh CI is running after maintainer approval of the fork workflow.

Review workflow: .claude/skills/how-to-review/SKILL.md.

[codecov]

Codecov Report

❌ Patch coverage is 99.46809% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 97.03%. Comparing base (48a9571) to head (40a445d).

Files with missing lines	Patch %	Lines
...unit_tests/rules/setsplitting_naesatisfiability.rs	99.27%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##             main    #1195    +/-   ##
========================================
  Coverage   97.03%   97.03%            
========================================
  Files        1103     1105     +2     
  Lines      145876   146064   +188     
========================================
+ Hits       141545   141736   +191     
+ Misses       4331     4328     -3     

☔ 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.

[GiggleLiu]

The reported blockers are resolved at 40a445d6162f25995042bd50365f31ff55a92464: the measured clause-variable bound is correct; SAT construction is checked and fallible; the directed proof and canonical example are complete; and exhaustive/adversarial regressions pass. Independent review, make check (7,093 tests), make paper, and the real CLI round trip pass. All nine fresh CI and Codecov checks pass. Approved for merge.