[isPANN]

⚠️ Critical: breaking change to KSatisfiability

This PR removes a public variant and two public constructors. Downstream code and stored instances that use them will break (see Migration).

Why

KSatisfiability<KN> checked no clause width, so it was Satisfiability under a second name. Its only edges were identity casts (K2 → KN, K3 → KN, KN → SAT), so every K-SAT path through SAT paid extra hops, e.g.

before: KSatisfiability/K2 → KSatisfiability/KN → Satisfiability → KSatisfiability/K3 → …
after:  KSatisfiability/K2 → Satisfiability → KSatisfiability/K3 → …

new_allow_less / try_new_allow_less let Rust code build K2/K3 instances with fewer than K literals per clause, which serde and the CLI already rejected. No rule produced such instances; only tests did. Every 3-SAT rule still had to handle them, and two parameter formulas had to stay upper_bound.

Changes

• Model: the KN variant is gone. K3 is the default variant. try_new requires exactly K literals per clause, and a KN instance fails with a construction error.
• Graph: the two K-SAT casts are deleted. K2 → SAT and K3 → SAT are now direct edges, and K2 → SAT has its own canonical example.
• Solver pipeline: the ILP pipeline that started from KSatisfiability/KN now starts from KSatisfiability/K3.
• Rules: short- and empty-clause branches are removed from DecisionMVC, KClique, BicliqueCover, CyclicOrdering, FeasibleRegisterAssignment, PreemptiveScheduling, RegisterSufficiency and QUBO.
• Exact again: 3SAT → KClique num_vertices = 3m+1 and 3SAT → DecisionMVC num_edges = n+6m.
• Now exact: 3SAT → MonochromaticTriangle vertex, edge and triangle counts. SAT → NAE turns every three-literal clause into a four-literal one, so the shorter-clause branch is gone.
• Simplify pass: each K-SAT ↔ SAT aggregate mapping is registered in the same macro as its witness edge. CyclicOrdering allocates its padding variables with allocate_many. Leftover short-clause comments and padding are removed from OneInThree, QuadraticCongruences and Kernel.
• Paper: the K-SAT cast entry is removed and the short/empty-clause cases are dropped from the affected proofs.
• Tests: short-clause inputs now repeat a literal ([1] → [1,1,1]). Tests that only covered empty clauses are removed. New tests check that wrong widths and KN are rejected.

Commits:

• 5e512c7: the main change.
• 86d6808: fixes from the agentic review.
• eafd02a: the simplify pass.
• 3c2f9bd: drops the FixedK trait that eafd02a added. It wasn't needed to remove the variant, so KSatisfiability keeps KValue with a runtime width check.

Migration

• KSatisfiability<KN>: use Satisfiability instead; it has the same JSON shape.
• Short clauses: use KSatisfiability::<K3>::new with repeated literals, e.g. [a, b] → [a, b, b].
• CLI: pred create KSAT now creates K3.
• pred-validation-corpus: the 100 instances under instances/KSatisfiability-KN need to move to Satisfiability. I'll do that in a follow-up corpus commit.

Verification

• cargo test --lib --all-features: 6321 passed (at 3c2f9bd)
• cargo test -p problemreductions-cli --all-features: all suites passed
• cargo test --test main: 80 passed
• cargo clippy --workspace --all-features --all-targets: 0 warnings
• make paper: builds with full rule coverage

Base: feat/exact-tight-bounds (#1224).

🤖 Generated with Claude Code

[isPANN]

Agentic Review Report

PR #1225 (refactor/remove-ksat-kn -> feat/exact-tight-bounds), head 5e512c73. This is a generic refactor review: it removes KSatisfiability<KN> and the short-clause constructors.

Structural

• KSatisfiability<KN> has been removed from declare_variants!, register_brute_force!, the schema dimension, and the ILP pipeline. K3 is now the default variant. try_new rejects any width other than K and also rejects an unfixed K (KN). Serde goes through try_new, so Rust, serde, and the CLI enforce the same constraint.
• ksatisfiability_casts.rs is deleted. impl_ksat_to_sat!(K2) and impl_ksat_to_sat!(K3) now register direct exact edges, each with its own aggregate registration. A K2 canonical example was added, and I checked its witness by hand.
• I found no leftover references to new_allow_less, try_new_allow_less, KSatisfiability<KN>, or ksatisfiability_casts. The remaining KN uses (KColoring, MaximumCoKPlex) are legitimate.
• No generated exports are in the diff, and I found no unrelated edits.

Semantic (traced by hand)

• DecisionMVC num_edges = n + 6m (exact): this holds. The graph has n truth-setting edges, 3 triangle edges per clause, and 3 communication edges per clause. Each communication edge (base+k, literal_vertex) starts from a different triangle vertex, so repeated literals still give distinct edges. For the empty formula the count is n.
• KClique num_vertices = 3m + 1 (exact): this holds for every strict-K3 input. Repeated literals still contribute 3 occurrence vertices per clause, and the empty formula gives 1 vertex with k = 1.
• Removed short-clause branches:
  • BicliqueCover, FeasibleRegisterAssignment, RegisterSufficiency, PreemptiveScheduling, and QUBO: all now index exactly 3 (or 2 for K2) literals. The removed padding was a no-op for width-K clauses.
  • PreemptiveScheduling: the empty-formula witness check (assignment.len() == num_vars) is correct.
  • CyclicOrdering: the [a,b] and [a] arms are still reachable after deduplication, so keeping them is right.
• I found no rule whose correctness depended on short clauses.

Quality

• New rejection paths are tested:
  • test_ksat_rejects_clause_widths_other_than_k covers widths 0, 1, 2, and 4.
  • test_ksat_rejects_unbounded_clause_width covers KN.
  • The CLI rejects 3SAT --clauses 1,2 with an actionable message.
  • Every short-clause test was rewritten to use repeated literals rather than deleted outright.
  • three_sat_counts_are_exact_on_repeated_literals checks the exact KClique and DMVC fields on the empty formula and on repeated-literal formulas.
• Targeted tests pass with -j 4 --lib --all-features: ksat (169), symbolic_parameter_contracts, parameter_formula, aggregate_contracts, ilp_overhead, example_db, and test_reduction_chain_with_variant.

Feature test (target/debug/pred)

• pred list shows two variants (aliases KSAT, 2SAT, 3SAT). pred show KSAT resolves to K3, and DMVC/KClique are now listed as exact.
• pred path 2SAT SAT returns a single direct step.
• The K2 example solves with brute force. The K3 example solves with --solver ilp through SAT -> NAE -> ILP.
• Loading a JSON instance with k: "KN" fails cleanly ("Known variants: K3, K2").

Findings

Critical: none.

Important

1. MonochromaticTriangle bounds are now exact but are still declared upper_bound (src/rules/ksatisfiability_monochromatictriangle.rs:76-81). With strict K3, every SAT clause becomes a 4-literal NAE clause, so q = m. That gives N = n+1+m and T = n+1+3m, which makes 16n+40m+16, 50n+146m+50, and 58n+174m+58 equalities for vertices, edges, and triangles. I confirmed this with pred on the canonical example (n=3, m=1): 104, 346, and 406, all equal to the formulas. Short clauses were the only reason these were upper bounds, which is the same situation as KClique and DMVC.
   • Fix: change to transform = exact { ... }, add the rule to three_sat_counts_are_exact_on_repeated_literals, and replace "Let q count its length-three clauses" in the paper (docs/paper/reductions.typ:17985) with q = m.

Minor (stale short- or empty-clause wording and dead code)
2. src/rules/ksatisfiability_oneinthreesatisfiability.rs:

• Lines 4-5 ("Missing native clause positions use the forced false variable") and lines 108-110 ("including the empty disjunction") are stale.
• Line 111, let mut literals = [z_false; 3]: the z_false padding is now dead because every position is overwritten.
• Fix: build [l1,l2,l3] directly from the three literals. In the paper (reductions.typ:18044), drop "Each native source clause has zero through three positions; fill missing positions with $z_0$ ... including the empty clause's false value".

3. QuadraticCongruences:
   • src/rules/ksatisfiability_quadraticcongruences.rs:5 says "widths zero through three"; after deduplicating a K3 clause the width is 1 to 3.
   • The paper (reductions.typ:12508, "retaining empty clauses", and :12517, "An empty clause has $T_j=0$ ...") still describes empty clauses, which strict K3 cannot contain.
4. MonochromaticTriangle:
   • The comment at src/rules/ksatisfiability_monochromatictriangle.rs:137-140 ("lengths 2, 3 and 4, including NAE(s,s) for an empty clause") is stale; from a K3 source only length 4 occurs, so the else branch is dead for this rule.
   • Paper step 1 (reductions.typ:17987) mentions the empty-clause case.
5. Kernel paper reductions.typ:19182 says "including the native short-clause semantics". This is stale now that every clause has exactly three occurrences.
6. Optional: src/solvers/pipelines.rs:280 registers an ILP pipeline only for K3, so KSatisfiability/K2 has ilp: null. This is not a regression, since only KN had a pipeline before. If you want parity, add a K2 pipeline (K2 -> SAT -> NAE -> ILP).

Verdict: the change is correct and approve-worthy. Please address item 1 (an exactness promotion that fits this branch's purpose) and the stale-text cleanups in items 2-5 before merging.

[isPANN]

Addressed the review in 86d6808.

Important

1. MonochromaticTriangle is now transform = exact. SAT → NAE turns every three-literal clause into a four-literal one, so the two-literal branch can no longer run. The loop now destructures [a, b, c, d], and auxiliary_count = nae.num_clauses(). The paper derives the counts exactly: substituting N = n+1+m and T = n+1+3m into 4N+12T, 2N+48T and 58T gives the three formulas. The rule is also checked in three_sat_counts_are_exact_on_repeated_literals.

Minor

2. OneInThree: fixed the stale module and code comments. The dead [z_false; 3] padding is now [0; 3], since every position is overwritten. Paper text fixed.
3. QuadraticCongruences: the module doc now says "deduplicated widths one through three". Removed the empty-clause wording in the paper.
4. MonochromaticTriangle: the stale NAE(s,s) comment and paper step 1 are fixed.
5. Kernel: removed "native short-clause semantics" from the paper.
6. A K2 ILP pipeline is left out of scope. It isn't a regression: before this PR, only KN had a pipeline.

Checks: lib tests 6321 passed, clippy 0 warnings, make paper OK.

[GiggleLiu]

Agentic Review Report

PR #1225 — [Critical] Remove KSatisfiability KN variant and short-clause constructors

Reviewed head 3c2f9bdaf00c0f265dc567f4b593b24f8c37a625 against its own stacked base ef18c7635bb68aa2bd36b41f995ed3c89c3db9db, not main. Read-only review from /tmp/problemreductions-review-ksat; no tracked edits, posts, pushes, or merges. The user explicitly accepted the public API break if checks pass.

Structural and semantic

• Scope is the intended API cleanup: 39 Rust/Typst source and test files, with the obsolete cast rule deleted. Inspected every diff, all changed production reduction/model implementations, related SAT-to-NAE and allocator implementations, and changed test contracts. Paper review covered the affected proof sections, not the entire paper. No new core trait/macro changes or generated exports.
• KSatisfiability::try_new validates literals and requires a fixed width and exactly K positions in every clause. Fields are private and getters expose immutable slices; serde uses the same constructor. Thus a constructible K2/K3 cannot reach the removed empty/short-clause arms. KN now fails even for an empty conjunction. Repeated literals and tautologies remain legal; an empty conjunction remains legal.
• K3 is consistently the registry/schema default; K2 and K3 now each have a direct exact embedding into SAT. The embedding preserves variables, clauses, literal counts, witness values, and aggregate Or values. Removing the KN casts shortens paths without introducing a K3-to-K2 reduction. The K3 ILP pipeline remains SAT -> NAE -> ILP. Lack of a K2 ILP pipeline predates this change.
• Traced the surviving branches in BicliqueCover, FeasibleRegisterAssignment, RegisterSufficiency, PreemptiveScheduling and QUBO: removing literal padding is a no-op on width-K input; removing fixed empty-clause NO instances is justified by construction rejection. Empty-conjunction YES handling survives. OneInThree initializes all three positions before use. CyclicOrdering correctly retains its one- and two-literal normalized cases: deduplication of [a,a,a] and [a,b,b] makes these reachable. allocate_many(3-len) gives the same fresh indices as the prior individual allocations, and tautologies are dropped before allocation.
• KClique's 3m+1 vertices and m+1 threshold are exact. Literal positions remain separate vertices even when variables repeat. Every valid threshold clique contains the anchor and one compatible occurrence per clause; extraction is consistent. clique_sizes checks the largest multiplication before allocation.
• DecisionMVC has exactly 2n+3m vertices and n+6m edges. The n variable edges, 3m triangle edges and 3m communication edges are pairwise distinct; repeated literals do not merge communication edges because their clause-position endpoints differ. The empty formula has n edges and cover threshold n.
• MonochromaticTriangle's exact promotion is sound. SAT -> NAE appends one sentinel and preserves every three-literal clause, so there are N=n+1+m logical variables after splitting and T=n+1+3m triples. Each triple contributes 12 vertices, 48 edges and 58 triangles; the signals contribute 4N vertices and 2N edges. Distinct private sender vertices prevent extra cross-sender triangles even when a signal is reused. Therefore the registered counts are exactly 16n+40m+16, 50n+146m+50, 58n+174m+58. The NAE-four-to-two-triples identity holds for all 16 Boolean inputs. Empty n=m=0 still produces the sentinel/sign-consistency gadget with counts (16,50,58).
• No new algorithmic complexity claim is introduced: registered K2/K3 bounds are preserved. The API/domain restriction and exact-count assertions above were checked directly, rather than inferred from tests or citations.

Quality and validation

• git diff --check passed. Repository search found no remaining uses of the removed constructors/cast module; KN appears in K-SAT only in its deliberate rejection test.
• Native validation at the reviewed head: cargo test --locked --lib --all-features ksat passed 169/169. Using the resulting copied test binary, symbolic_parameter_contracts passed 28, parameter_formula 8, aggregate_contracts 14, ilp_overhead 51, test_reduction_graph 72, registry 107, example_db 66, and test_reduction_chain_with_variant 1, all with zero failures. These filters overlap; together they cover 510 distinct passing tests. Logs are test-1225-*.log in this report directory. Built with Rust 1.98.0, jobs=2, debug=0, incremental=0; subsequent filters used test-threads=2.
• Verification environment: the first build reused an older shared-target Expr artifact and reported a missing Sum implementation even though the reviewed source contained it. A selective cargo clean -p problemreductions-expr caused Expr, macros and the library to rebuild from the reviewed sources; the clean rebuild and tests passed. This was a cache artifact, not a PR defect.
• Independent combinatorial probe: all 4,162 formulas consisting of the empty formula, every ordered three-literal clause and pair over two variables, plus the zero-variable empty formula, satisfy the new MonochromaticTriangle and DecisionMVC counts. Also checked the NAE splitting identity on all 16 Boolean tuples. Evidence: ksat-exact-counts-probe.py and ksat-exact-counts-probe.txt in this report directory. This checks mathematical graph counts independently; it does not substitute for native Rust execution.
• Existing tests preserve coverage of repeated/complementary literals, sparse variables, empty conjunctions, UNSAT instances, malformed target witnesses and numeric count limits. Exhaustive small-target checks remain for KClique, Kernel and QUBO. Invalid-width tests replace the now-impossible empty/short clause construction cases. No coverage percentage was measured.

Feature test

Exact-head native registry, aggregate mapping, symbolic parameter, path-chain and canonical example tests all passed, as listed above. The PR's author reports CLI, all-library, integration, Clippy and paper checks; those reports are not independent verification. No fresh exact-head CLI install or complete paper build was performed by this reviewer. API migration is explicitly documented in the PR body: use Satisfiability for former KN, repeat literals for short K2/K3 clauses, and migrate the external KN validation corpus.

Findings

Critical: no new issue found in this PR's own diff.

Important: no new issue found in this PR's own diff. This is not a merge clearance for the stack: #1224 and earlier growth/UI findings remain dependency blockers and must be resolved/reviewed separately.

Minor — remaining paper wording still advertises removed native clause widths.

• docs/paper/reductions.typ:12506 says the QuadraticCongruences construction handles native widths zero through three. The native K3 input now has exactly three positions; deduplication leaves one through three.
• docs/paper/reductions.typ:18134 says RegisterSufficiency extends to the native zero-to-three-literal domain, contradicting the new constructor.
• docs/paper/reductions.typ:19180 still mentions missing Kernel clause positions being set false; none can be missing now.

Suggested fix: describe exact-three native inputs with repeated literals, distinguish normalized widths where applicable, and delete the obsolete missing-position phrase. These are documentation cleanups, not mathematical blockers.

GitHub PR Audit

GATE: PASS for harm signals. Code correctness and inherited dependency findings are assessed separately.

• harm.secrets (security.no-secrets): OK — reviewed added lines; no credentials, private keys or sensitive personal data found; bounded signature scan had no hits.
• harm.dangerous-files (git.harm-signals): OK — only relevant Rust and Typst files; no conflict markers, archives, binaries, local configurations or scratch files in diff. Worktree status clean.
• harm.generated-artifacts (code.generated-artifacts): OK — no generated exports, build/target/dependency outputs added.
• harm.cache (code.generated-cache): OK — no caches added.
• harm.debug-leftovers (code.debug-leftovers): OK — no new debug probes, breakpoints or WIP markers found.
• pr.description-quality (github.pr-description-quality): OK — explains purpose, API break, migration, tests and stack base in detail.
• pr.traceable (github.prs-traceable): OK — clear motivation, migration consequences and base #1224, with review/fix history.

Verdict

Own diff: acceptable with minor documentation advice after independent native checks. Keep the PR open as dependency-blocked, consistent with the user’s decision to leave substantive blockers and their dependent stack open. The accepted API break is intentional. No new substantive blocker was found; only the minor paper wording above is newly reported here. This is not blanket validation of the inherited stack or a claim that the full 6,321-test suite was independently rerun.

[GiggleLiu]

Review follow-up

Pushed proof correction 9b281d770: the quadratic-congruence, exact-one, register-sufficiency, and kernel proofs now describe the exact-width native K3 domain. Normalization can still shorten quadratic-congruence clauses. Independent review found no issue with the correction.

The complete repaired stack passed 7,194 native tests, formatting, Clippy, and the paper build at d96e7c8b84733dbdd5873e19b8bf1185c7e7396d. The numeric prerequisite in #1224 is fixed and tested. Full website and final main CI checks are still pending.

Compatibility note for the next release: KSAT defaults to K3; KSatisfiability<KN> and short-clause constructors are removed. Persisted KN instances require migration.

[GiggleLiu]

Agentic Review Report: stack consolidation

Approved reviewed head 9b281d770bd1a37cb823a2c7e041beae161ae7a8 for merging into feat/exact-tight-bounds only. The user accepted the K-SAT API migration. The proof wording correction is reviewed, and the numeric prerequisite is fixed at 52bd171a0.

Checked inline comments, submitted reviews, PR conversation, linked-issue comments, and Codecov comments. No new unaddressed material finding. Harm gate remains PASS from the independent review.

The repaired combined stack passed 7,194 native tests, formatting, all-target/all-feature Clippy, and make paper at d96e7c8b8. Those results include the separate semantic fixture correction; they are aggregate validation, not a claim that this individual head was retested unchanged. Final website checks and strict main-branch CI remain pending. This merge preserves the PR record while consolidating the reviewed backend stack.