[montionugera]

Closes #1101

Summary

• Implemented the direct clause-doubling reduction from NAESatisfiability to Satisfiability (src/rules/naesatisfiability_satisfiability.rs), mapping each NAE clause (l_1, ..., l_r) to (l_1 OR ... OR l_r) and (not l_1 OR ... OR not l_r) over the same n variables with identity witness extraction.
• Registered overhead formulas (num_vars, 2 * num_clauses, 2 * num_literals) and paper documentation (docs/paper/reductions.typ).
• Added unit tests in src/unit_tests/rules/naesatisfiability_satisfiability.rs covering the empty conjunction, canonical 3-variable truth-table equivalence across all 8 assignments, monochromatic 1-variable unsatisfiable clause, repeated literals, tautological clauses, and higher-arity clauses.

[GiggleLiu]

Agentic Review Report

Reviewed PR #1210 at 43fb5e0d629d6724b975ff07e8ac6e806d3a6e22 against merge base 875b6e86d5a87e5f66c2f6743be9d22abe917a09.

Structural and semantic

No semantic finding. Each NAE clause and its literalwise complement jointly enforce at least one true and one false literal, including repeated and complementary literals. The source constructor excludes i64::MIN, so unary negation is safe. The target constructor is fallible and preserves its typed construction error. Identity extraction first requires a satisfying target assignment. The three exact target counts match the construction.

Module registration, identity aggregate mapping, canonical example collection, dedicated example lookup test, unit-test linkage, and a directed paper theorem are present. The canonical instance matches issue #1101. The existing registry-wide parameter test discovers the new example, so no separate hardcoded registration in that test is needed.

Quality and findings

• Minor, required formatting check fails: src/unit_tests/rules/naesatisfiability_satisfiability.rs:105. cargo fmt --all -- --check requests wrapping the chained extract_solution(...).unwrap() call. Apply Rustfmt and rerun the check.
• Unit tests cover all canonical assignments, mixed arities with five variables, repeated literals, tautologies, an unsatisfiable clause, empty conjunctions including zero variables, rejecting assignments, malformed witness lengths, and closed-loop solves.
• git diff --check passed.

Feature test and validation limits

No Rust test binary or CLI was built by this reviewer while the parent serialized memory-intensive builds. No CI checks have executed on this head. Before merging, run the focused rule tests, canonical-example lookup/consistency test, and executable parameter-formula check after the formatting fix. A CLI example/reduce/solve round trip would complete the repository workflow.

Verdict

Semantically safe on static review. Hold merging until the mechanical formatting fix and runtime validation complete.

GitHub PR audit

GATE: PASS

• harm.secrets: OK. No credential material.
• harm.dangerous-files: OK. Purposeful source, theorem, 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 lists tests but does not state commands actually run or results.
• pr.traceable: OK. Links issue #1101 and describes the clause-doubling construction.

Integration follow-up

Prepared detached merge commit 260c6290f09a4fc24cc71800b48a91d7d4860494 on current main 35f40b49fb36855537661ec08f3b2480a4fbb67f. The only conflict kept the new example lookup test and removed an obsolete comment. Rustfmt fixed the reported line wrap. cargo fmt --all -- --check and git diff --check now pass. A literal-aware comparison of all 483 changed Rust files against the reviewed PR head found identical noncomment tokens after optional trailing-comma normalization. The worktree is clean. Runtime tests are still pending the shared compile slot. No push was performed by this reviewer.

Completed validation and final verdict

The pending conditions above are now satisfied on 260c6290f09a4fc24cc71800b48a91d7d4860494. All 11 focused rule/canonical-lookup tests passed, as did the canonical rule solution-pair consistency test and the global executable parameter-formula test. The local CLI build passed. In a scratch directory, canonical example creation, inspect, direct brute-force solve, direct NAE→SAT route discovery, reduction, bundle solve, and recovered source reevaluation all passed. Both solves returned Or(true) with [false, false, true]. Artifacts are in /tmp/problemreductions-pr-review-20261029/cli-1210.

Final verdict: safe to merge the integrated commit after parent publication/current-head checks. The previous hold is resolved. The reviewer committed only the authorized main merge and mechanical formatting fix; no push was performed.

Integration and runtime verification

Reviewed updated head 260c6290f09a4fc24cc71800b48a91d7d4860494. Merged main comment cleanup and formatted the single chained call. All 483 changed Rust files preserve noncomment tokens relative to the initially reviewed head, allowing optional trailing commas. Formatting and diff-whitespace checks pass. Eleven focused rule/lookup tests, canonical rule solution-pair consistency and the executable parameter-formula test all passed. Built the CLI and completed canonical create, inspect, direct brute-force solve, persisted direct route/reduction, bundle solve and source reevaluation. Both workflows returned Or(true) with source witness [false, false, true]. The formatting finding above is resolved. Await fresh CI before merge.

[codecov]

Codecov Report

❌ Patch coverage is 99.50249% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 97.03%. Comparing base (8622b3f) to head (c963cd6).

Files with missing lines	Patch %	Lines
src/rules/naesatisfiability_satisfiability.rs	97.82%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##             main    #1210    +/-   ##
========================================
  Coverage   97.02%   97.03%            
========================================
  Files        1101     1103     +2     
  Lines      145675   145876   +201     
========================================
+ Hits       141342   141545   +203     
+ Misses       4333     4331     -2     

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

Agentic Review Report

Reviewed PR #1210 at 43fb5e0d629d6724b975ff07e8ac6e806d3a6e22 against merge base 875b6e86d5a87e5f66c2f6743be9d22abe917a09.

Structural and semantic

No semantic finding. Each NAE clause and its literalwise complement jointly enforce at least one true and one false literal, including repeated and complementary literals. The source constructor excludes i64::MIN, so unary negation is safe. The target constructor is fallible and preserves its typed construction error. Identity extraction first requires a satisfying target assignment. The three exact target counts match the construction.

Module registration, identity aggregate mapping, canonical example collection, dedicated example lookup test, unit-test linkage, and a directed paper theorem are present. The canonical instance matches issue #1101. The existing registry-wide parameter test discovers the new example, so no separate hardcoded registration in that test is needed.

Quality and findings

• Minor, required formatting check fails: src/unit_tests/rules/naesatisfiability_satisfiability.rs:105. cargo fmt --all -- --check requests wrapping the chained extract_solution(...).unwrap() call. Apply Rustfmt and rerun the check.
• Unit tests cover all canonical assignments, mixed arities with five variables, repeated literals, tautologies, an unsatisfiable clause, empty conjunctions including zero variables, rejecting assignments, malformed witness lengths, and closed-loop solves.
• git diff --check passed.

Feature test and validation limits

No Rust test binary or CLI was built by this reviewer while the parent serialized memory-intensive builds. No CI checks have executed on this head. Before merging, run the focused rule tests, canonical-example lookup/consistency test, and executable parameter-formula check after the formatting fix. A CLI example/reduce/solve round trip would complete the repository workflow.

Verdict

Semantically safe on static review. Hold merging until the mechanical formatting fix and runtime validation complete.

GitHub PR audit

GATE: PASS

• harm.secrets: OK. No credential material.
• harm.dangerous-files: OK. Purposeful source, theorem, 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 lists tests but does not state commands actually run or results.
• pr.traceable: OK. Links issue #1101 and describes the clause-doubling construction.

Integration follow-up

Prepared detached merge commit 260c6290f09a4fc24cc71800b48a91d7d4860494 on current main 35f40b49fb36855537661ec08f3b2480a4fbb67f. The only conflict kept the new example lookup test and removed an obsolete comment. Rustfmt fixed the reported line wrap. cargo fmt --all -- --check and git diff --check now pass. A literal-aware comparison of all 483 changed Rust files against the reviewed PR head found identical noncomment tokens after optional trailing-comma normalization. The worktree is clean. Runtime tests are still pending the shared compile slot. No push was performed by this reviewer.

Completed validation and final verdict

The pending conditions above are now satisfied on 260c6290f09a4fc24cc71800b48a91d7d4860494. All 11 focused rule/canonical-lookup tests passed, as did the canonical rule solution-pair consistency test and the global executable parameter-formula test. The local CLI build passed. In a scratch directory, canonical example creation, inspect, direct brute-force solve, direct NAE→SAT route discovery, reduction, bundle solve, and recovered source reevaluation all passed. Both solves returned Or(true) with [false, false, true]. Artifacts are in /tmp/problemreductions-pr-review-20261029/cli-1210.

Final verdict: safe to merge the integrated commit after parent publication/current-head checks. The previous hold is resolved. The reviewer committed only the authorized main merge and mechanical formatting fix; no push was performed.

Integration and runtime verification

Reviewed updated head 260c6290f09a4fc24cc71800b48a91d7d4860494. Merged main comment cleanup and formatted the single chained call. All 483 changed Rust files preserve noncomment tokens relative to the initially reviewed head, allowing optional trailing commas. Formatting and diff-whitespace checks pass. Eleven focused rule/lookup tests, canonical rule solution-pair consistency and the executable parameter-formula test all passed. Built the CLI and completed canonical create, inspect, direct brute-force solve, persisted direct route/reduction, bundle solve and source reevaluation. Both workflows returned Or(true) with source witness [false, false, true]. The formatting finding above is resolved. Await fresh CI before merge.

Combined integration validation

The reviewed change was also validated with the other safe candidates at Rust 2024 integration head 3e768b37bc54efc5af4d133b3162efdc7ecfb27f: workspace/all-feature tests and the ignored-only follow-up passed all 7,161 tests; all-target/all-feature Clippy with warnings denied, formatting, diff check, and 23 Python tests passed. Independent semantic-baseline token comparison verified the merge resolutions. Details and logs are in review-1207-integration.md and the adjacent *-1207-integrated*.log artifacts.

Current-main update

Current reviewed head is c963cd6e1d7ef649059e55e4d9b9dc1b43ba8b91. It merges current main cleanly. Its tree fe369733293884a95ead063f36f7f72e929d03ee matches the independently inspected semantic integration baseline exactly; the NAE rule and tests are unchanged. Fresh current-head CI is the remaining merge gate.