diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ
index 9fcc31655..947d23aba 100644
--- a/docs/paper/reductions.typ
+++ b/docs/paper/reductions.typ
@@ -12465,11 +12465,11 @@ _Solution extraction and bounds._ Decode a string permutation, concatenate with
   $ H = a y_3 + 2(y_1 y_2 - 2 y_1 a - 2 y_2 a + 3a). $
   Rosenberg's penalty is zero when $a=y_1 y_2$ and positive otherwise @borosgruber2014quadratization. Its multiplier 2 strictly exceeds the possible unit gain from the $a y_3$ term. Thus minimizing over each independent auxiliary gives exactly the clause falsification indicator, including repeated or complementary literals. Expand with $x^2=x$ into an upper-triangular QUBO matrix, and retain the omitted constant $C$.
 
-  _Correctness._ For every source assignment, the minimum target energy over auxiliaries is the number of falsified clauses minus $C$. Every clause expression is nonnegative before subtracting $C$. Hence the formula is satisfiable iff the global target minimum is exactly $-C$. A satisfying assignment lifts by setting each cubic auxiliary to $y_1 y_2$; every zero-penalty target configuration projects to a satisfying source assignment. If an empty clause occurs, its constant penalty 1 prevents the threshold from being attained. Empty formulas have $C=0$ and every source assignment satisfies them.
+  _Correctness._ For every source assignment, the minimum target energy over auxiliaries is the number of falsified clauses minus $C$. Every clause expression is nonnegative before subtracting $C$. Hence the formula is satisfiable iff the global target minimum is exactly $-C$. A satisfying assignment lifts by setting each cubic auxiliary to $y_1 y_2$; every zero-penalty target configuration projects to a satisfying source assignment. Empty formulas have $C=0$ and every source assignment satisfies them.
 
   _Extraction._ Formal target validation precedes decoding. The DecisionQUBO target checks the bound $E <= -C$, and the registered aggregate decoder maps its completed `Or` value identically. Direct witness extraction rejects energies above the bound and reads the first $n$ coordinates only for a satisfying target witness. It does not solve SAT or repair auxiliary assignments. A completed target decision gives the source decision.
 
-  _Domain and overhead._ The K2 variant has $n$ variables; K3 reserves $n+m$, with unused auxiliaries mathematically free for short clauses. Native `new_allow_less` permits widths up to K; CLI and serde still require exactly K per actual clause. Source and target both use `Or`; the target wraps the integer QUBO with the signed bound $-C$. Matrix and constant accumulation use checked arithmetic; literal indices come from the formal `CNFClause::variables` API. Neither endpoint nor variant changes.
+  _Domain and overhead._ The K2 variant has $n$ variables; K3 reserves $n+m$, one auxiliary per clause. Every clause has exactly K literals. Source and target both use `Or`; the target wraps the integer QUBO with the signed bound $-C$. Matrix and constant accumulation use checked arithmetic; literal indices come from the formal `CNFClause::variables` API. Neither endpoint nor variant changes.
 ]
 
 #let ksat_qc = load-example("KSatisfiability", "QuadraticCongruences")
@@ -12503,9 +12503,9 @@ _Solution extraction and bounds._ Decode a string permutation, concatenate with
     *Multiplicity:* The fixture stores one canonical satisfying witness.
   ],
 )[
-  The bounded quadratic-congruence construction of Manders and Adleman @mandersAdleman1976 converts an odd signed-knapsack target into a square congruence using prime powers and the Chinese Remainder Theorem. We give base-eight positions only to the actual normalized clauses. The same slack equation handles every native clause width from zero through three.
+  The bounded quadratic-congruence construction of Manders and Adleman @mandersAdleman1976 converts an odd signed-knapsack target into a square congruence using prime powers and the Chinese Remainder Theorem. We give base-eight positions only to the actual normalized clauses. The same slack equation handles clauses of at most three literals after normalization.
 ][
-  _Construction._ Delete tautologies and duplicate literals and clauses, retaining empty clauses. Compact the $l$ occurring variables, recording their original positions. Let $C_1, dots, C_m$ be the remaining clauses, $r_j = |C_j|$, $N = 2m+l+1$, and $D=8^(m+1)$. Let $f_i^+$ and $f_i^-$ be the sums of $8^j$ over clauses containing variable $i$ positively and negatively. Define $N$ integer coefficients and an odd target:
+  _Construction._ Delete tautologies and duplicate literals and clauses. Compact the $l$ occurring variables, recording their original positions. Let $C_1, dots, C_m$ be the remaining clauses, $r_j = |C_j|$, $N = 2m+l+1$, and $D=8^(m+1)$. Let $f_i^+$ and $f_i^-$ be the sums of $8^j$ over clauses containing variable $i$ positively and negatively. Define $N$ integer coefficients and an odd target:
   $ c_0=1, quad c_(2j-1)=-8^j/2, quad c_(2j)=-8^j, quad c_(2m+i)=(f_i^+-f_i^-)/2, $
   $ tau=1+sum_(j=1)^m (r_j-5)8^j/2. $
   Take the first $N$ primes starting at $13$, indexed from zero, and put $q_i=p_i^N$ and $K=product_i q_i$. Let $theta_i$ be the least positive integer satisfying $theta_i equiv c_i mod D$, $theta_i equiv 0 mod (K/q_i)$, and $p_i$ not dividing $theta_i$. CRT gives a residue modulo $D K/q_i$; choosing the first positive representative and, if necessary, adding that modulus once gives $theta_i$. Set $H=sum_i theta_i$ and
@@ -12514,7 +12514,7 @@ _Solution extraction and bounds._ Decode a string permutation, concatenate with
 
   _Clause encoding._ For signs $alpha_i in {-1,+1}$, put $t_i=(1-alpha_(2m+i))/2$ and $y_j=(3-alpha_(2j-1)-2alpha_(2j))/2 in {0,1,2,3}$. Let $T_j$ count true literals in $C_j$ and $R_j=y_j-T_j+1$. Direct expansion gives
   $ sum_i c_i alpha_i-tau=alpha_0-1+sum_(j=1)^m R_j 8^j. $
-  Here $-2<=R_j<=4$ and $alpha_0-1 in {-2,0}$. The right side has absolute value less than $D$. Taking successive residues modulo eight shows that it vanishes exactly when $alpha_0=1$ and all $R_j=0$. Thus the linear congruence modulo $D$ encodes precisely the satisfying assignments. An empty clause has $T_j=0$ and cannot have $R_j=0$; it requires no exceptional construction.
+  Here $-2<=R_j<=4$ and $alpha_0-1 in {-2,0}$. The right side has absolute value less than $D$. Taking successive residues modulo eight shows that it vanishes exactly when $alpha_0=1$ and all $R_j=0$. Thus the linear congruence modulo $D$ encodes precisely the satisfying assignments.
 
   _Magnitude and square-root lemmas._ Each $theta_i<=2D K/q_i$. For $m>=1$, $N>=2m+1>=3$ and $13^N>4N D$, giving $2H<K$. When $m=0$, no variable occurs, and $N=1$, $theta_0=1$, $K=13$ give the same inequality. Also $tau equiv 1 mod 4$ and $D$ is a power of two divisible by eight. For odd $tau$, $x^2 equiv tau^2 mod (2D)$ holds exactly when $x equiv tau$ or $x equiv -tau mod D$: among $x-tau$ and $x+tau$, one has exactly one factor of two and the other must contain all the remaining factors. This is the odd-target hypothesis of the original square-root lemma; doubling the coefficients without increasing the square modulus does not preserve it.
 
@@ -17306,16 +17306,6 @@ Problems parameterized by graph type, weight type, target type, or clause width
   _Solution extraction._ Return the target configuration unchanged.
 ]
 
-#reduction-rule("KSatisfiability", "KSatisfiability")[
-  A $k$-SAT instance with fixed clause width ($k = 2$ or $k = 3$) converts to generic $k$-SAT by constructing the registered $K_N$ variant. The clauses and variables are preserved verbatim; the target uses `new_allow_less` to accept clauses with fewer than $k$ literals.
-][
-  _Construction._ Given $"KSat"_(K_j)(n, cal(C))$ with $j in {2, 3}$, construct $"KSat"_(K_N)(n, cal(C))$ with the same $n$ variables and clause set $cal(C)$.
-
-  _Correctness._ Every clause in $cal(C)$ has at most $j$ literals. The $K_N$ variant accepts clauses of any width, so all clauses remain valid. The satisfiability condition (every clause has at least one true literal) is unchanged.
-
-  _Solution extraction._ Return the target configuration unchanged.
-]
-
 #reduction-rule("SpinGlass", "SpinGlass")[
   An Ising spin-glass instance with integer couplings and fields ($J_(i j), h_i in ZZ$) converts to the floating-point variant ($J_(i j), h_i in RR$) through exact `i64_to_exact_f64` embeddings. The graph topology is preserved.
 ][
@@ -17936,7 +17926,7 @@ The following table shows concrete target-variable counts for example instances,
 )[
   Use the classical 3-SAT to Vertex Cover gadget construction, then ask whether the resulting graph has a vertex cover of size at most $k = n + 2m$ @garey1979.
 ][
-  _Construction._ Given 3-CNF $phi$ with $n$ variables and $m$ clauses, build the graph $G = (V, E)$ used in the classical 3-SAT $arrow.r$ Minimum Vertex Cover reduction: for each variable $x_i$, add literal vertices $u_i$ and $overline(u)_i$ with one truth-setting edge between them; for each clause $c_j$, add triangle vertices $t^j_0, t^j_1, t^j_2$; for each literal position $(j, r)$, add a communication edge from $t^j_r$ to the literal vertex representing that literal. Assign unit weight to every vertex and set the decision threshold to $k = n + 2m$. For accepted short nonempty clauses, repeat their literals to fill three positions. For an empty clause, keep its triangle without communication edges and use threshold $-1$, making the decision instance infeasible. The vertex count stays exact; the edge count is at most $n+6m$.
+  _Construction._ Given 3-CNF $phi$ with $n$ variables and $m$ clauses, build the graph $G = (V, E)$ used in the classical 3-SAT $arrow.r$ Minimum Vertex Cover reduction: for each variable $x_i$, add literal vertices $u_i$ and $overline(u)_i$ with one truth-setting edge between them; for each clause $c_j$, add triangle vertices $t^j_0, t^j_1, t^j_2$; for each literal position $(j, r)$, add a communication edge from $t^j_r$ to the literal vertex representing that literal. Assign unit weight to every vertex and set the decision threshold to $k = n + 2m$. The graph has exactly $2n+3m$ vertices and $n+6m$ edges.
 
   _Correctness._ ($arrow.r.double$) If $phi$ is satisfiable, choose one literal vertex per variable according to a satisfying assignment and choose two triangle vertices per clause, omitting a vertex whose literal is true. This gives a cover of size $n + 2m$, so the decision instance is yes. ($arrow.l.double$) If the decision instance is yes, any cover of size at most $n + 2m$ must use exactly one literal vertex per variable edge and exactly two vertices per clause triangle. The omitted triangle vertex in each clause has its communication edge covered only by a selected literal vertex, so the corresponding literal is true. These selected literal vertices define a satisfying assignment for $phi$.
 
@@ -17992,14 +17982,14 @@ The following table shows concrete target-variable counts for example instances,
 
   Conversely, either equal signal colouring extends: make that colour the cycles $u,v,w,a,b,u$ and $u,v,w,c,d,u$ in the two cliques, and give all remaining edges the other colour. Both cycles agree on the private triangle, and each clique has no monochromatic triangle. No triangle crosses between the two signal edges.
 
-  _Construction._ Let the source have $n$ variables and $m$ clauses of length at most three; the typed API also admits shorter clauses. Let $q$ count its length-three clauses.
+  _Construction._ Let the source have $n$ variables and $m$ clauses, each with three literal positions.
 
-  1. Apply the existing typed embedding into Satisfiability and the existing SAT-to-NAE reduction. It adds a sentinel $s$, replacing each nonempty clause $C$ by $"NAE"(C,s)$ and an empty clause by $"NAE"(s,s)$.
-  2. Replace $"NAE"(a,b)$ by $"NAE"(a,b,b)$; keep triples unchanged; replace $"NAE"(a,b,c,d)$ by $"NAE"(a,b,z)$ and $"NAE"(overline(z),c,d)$ with a fresh variable $z$. There are $N=n+1+q$ logical variables and $m+q$ resulting triples.
-  3. Give every logical variable $i$ two disjoint signal edges $P_i,M_i$. Their $4N$ vertices are disjoint from all subsequent clause vertices. For each variable include the sign-consistency triple $"NAE"(P_i,P_i,M_i)$, followed by the logical triples, using $P_i$ for a positive literal and $M_i$ for a negative one. There are $T=N+m+q$ triples in total.
+  1. Apply the existing typed embedding into Satisfiability and the existing SAT-to-NAE reduction. It adds a sentinel $s$, replacing each clause $C$ by the four-literal $"NAE"(C,s)$.
+  2. Replace each $"NAE"(a,b,c,d)$ by $"NAE"(a,b,z)$ and $"NAE"(overline(z),c,d)$ with a fresh variable $z$. There are $N=n+1+m$ logical variables and $2m$ resulting triples.
+  3. Give every logical variable $i$ two disjoint signal edges $P_i,M_i$. Their $4N$ vertices are disjoint from all subsequent clause vertices. For each variable include the sign-consistency triple $"NAE"(P_i,P_i,M_i)$, followed by the logical triples, using $P_i$ for a positive literal and $M_i$ for a negative one. There are $T=N+2m$ triples in total.
   4. Give every triple its own triangle. Connect its three edges to the three literal signals using three equality senders, each with fresh private vertices. The terminal edges already exist, so a sender adds three vertices and fifteen edges. Repeated literals use separate senders; no endpoint identification or case-specific repair is performed.
 
-  _NAE identities._ The length-two identity holds because duplicating a value does not change whether all values agree. For the length-four identity, if $a=b$ the first triple forces $z=overline(a)$; if $c=d$ the second forces $z=c$. These requirements conflict exactly when all four values agree. If either pair differs, its corresponding triple imposes no condition on $z$. This proves the identity in both directions for all input patterns.
+  _NAE identity._ For the length-four identity, if $a=b$ the first triple forces $z=overline(a)$; if $c=d$ the second forces $z=c$. These requirements conflict exactly when all four values agree. If either pair differs, its corresponding triple imposes no condition on $z$. This proves the identity in both directions for all input patterns.
 
   _Triangle isolation._ Private vertices from different senders are nonadjacent. Any triangle containing a private sender vertex must lie in that sender: both other vertices belong to it, and the only edges among its four boundary vertices are its two terminal edges. This remains true after assembly because all variable signals and clause triangles have disjoint vertex sets, and senders add no boundary-to-boundary edges. A triangle containing no sender-private vertex is one of the clause triangles. Hence the target contains exactly the intended clause triangles and the nineteen triangles inside each sender, even with repeated or complementary literals and repeated variable occurrences.
 
@@ -18009,7 +17999,7 @@ The following table shows concrete target-variable counts for example instances,
 
   _Solution extraction._ Validate the target colouring and read the positive signal colours for the original variables and sentinel. Pass this assignment to the existing SAT-to-NAE extraction API. A global colour swap leaves the normalized source assignment unchanged.
 
-  _Overhead._ The exact counts are $4N+12T$ vertices, $2N+48T$ edges and $58T$ triangles. Since $q<=m$, these are bounded by $16n+40m+16$, $50n+146m+50$ and $58n+174m+58$, respectively. All graph-size arithmetic is checked before allocation. With exactly three literals per clause the bounds are equalities.
+  _Overhead._ The exact counts are $4N+12T$ vertices, $2N+48T$ edges and $58T$ triangles. Substituting $N=n+1+m$ and $T=n+1+3m$ gives exactly $16n+40m+16$, $50n+146m+50$ and $58n+174m+58$, respectively. All graph-size arithmetic is checked before allocation. With exactly three literals per clause the bounds are equalities.
 
   _YES example._ For the clause $(x_1 or x_2 or x_3)$, choose values $(1,0,0)$, sentinel $0$ and splitting variable $0$. Both logical triples evaluate to $"NAE"(1,0,0)$. Here $N=5$, $T=7$, giving 104 vertices, 346 edges and 406 triangles. The signal colours extend by the sender construction.
 
@@ -18051,16 +18041,16 @@ The following table shows concrete target-variable counts for example instances,
 )[
   Schaefer's Lemma 3.5 @schaefer1978 expresses a three-input disjunction by five exact-one constraints. The implementation compacts the $a$ appearing source variables, adds two global constant variables and six auxiliaries per clause. A source with $m$ clauses produces $a + 2 + 6m$ target variables and $1 + 5m$ target clauses, bounded by $n + 2 + 6m$ and $1 + 5m$ in the declared source parameters.
 ][
-  _Construction._ Let $J$ be the sorted original indices of the appearing variables. Replace each actual source literal by the corresponding compact variable with its sign preserved. Use the existing SAT variable allocator to allocate $z_0$ and $z_T$, followed by six fresh variables $a_j, b_j, c_j, d_j, e_j, f_j$ for each source clause. The global exact-one constraint $R(z_0,z_0,z_T)$ forces $(z_0,z_T)=(0,1)$. Each native source clause has zero through three positions; fill missing positions with $z_0$. This preserves its disjunction, including the empty clause's false value. For the resulting three literals $ell_1^j,ell_2^j,ell_3^j$, append
+  _Construction._ Let $J$ be the sorted original indices of the appearing variables. Replace each actual source literal by the corresponding compact variable with its sign preserved. Use the existing SAT variable allocator to allocate $z_0$ and $z_T$, followed by six fresh variables $a_j, b_j, c_j, d_j, e_j, f_j$ for each source clause. The global exact-one constraint $R(z_0,z_0,z_T)$ forces $(z_0,z_T)=(0,1)$. For each clause's three literals $ell_1^j,ell_2^j,ell_3^j$, append
   $
     R(ell_1^j,a_j,d_j), quad R(ell_2^j,b_j,d_j), quad
     R(a_j,b_j,e_j), quad R(c_j,d_j,f_j), quad R(ell_3^j,c_j,z_0).
   $
   Here $R$ counts literal occurrences, so its repeated $z_0$ in the global constraint is intentional. Negative literals remain permitted by the target model. Every clause uses this same construction; no empty-clause target case is needed.
 
-  _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, assign its appearing coordinates to the compact target variables and set the constants as above. Let $(x,y,z)$ be one padded clause's literal truth values. Set $d=(1-x)(1-y)$, $a=1-x-d$, $b=1-y-d$, $c=1-z$, $e=1-a-b$ and $f=z-d$. If $x=y=0$, satisfaction forces $z=1$, giving $(a,b,c,d,e,f)=(0,0,0,1,1,0)$. Otherwise $d=0$, $a=1-x$, $b=1-y$, $e=x+y-1$, and $f=z$; these and $c=1-z$ are Boolean because $x+y>=1$. Substitution gives $x+a+d=y+b+d=a+b+e=c+d+f=z+c=1$, satisfying all five constraints. Auxiliary variables are disjoint across clauses, so the assignments combine.
+  _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, assign its appearing coordinates to the compact target variables and set the constants as above. Let $(x,y,z)$ be one source clause's literal truth values. Set $d=(1-x)(1-y)$, $a=1-x-d$, $b=1-y-d$, $c=1-z$, $e=1-a-b$ and $f=z-d$. If $x=y=0$, satisfaction forces $z=1$, giving $(a,b,c,d,e,f)=(0,0,0,1,1,0)$. Otherwise $d=0$, $a=1-x$, $b=1-y$, $e=x+y-1$, and $f=z$; these and $c=1-z$ are Boolean because $x+y>=1$. Substitution gives $x+a+d=y+b+d=a+b+e=c+d+f=z+c=1$, satisfying all five constraints. Auxiliary variables are disjoint across clauses, so the assignments combine.
 
-  ($arrow.l.double$) Every target solution forces $z_0=0$. If a padded clause had $x=y=z=0$, the final constraint would force $c=1$; the fourth would then force $d=f=0$. The first two would force $a=b=1$, contradicting the third. Thus every padded disjunction is true, which implies every original clause is true. Repetition, opposite signs and missing positions do not change this argument.
+  ($arrow.l.double$) Every target solution forces $z_0=0$. If a source clause had $x=y=z=0$, the final constraint would force $c=1$; the fourth would then force $d=f=0$. The first two would force $a=b=1$, contradicting the third. Thus every source clause is true. Repeated literals and opposite signs do not change this argument.
 
   _Solution extraction._ Validate the target assignment once using the formal evaluator and reject $"Or(false)"$. Initialize a length-$n$ false vector, then restore the compact source coordinates to their original positions in $J$. Unused source variables stay false. The resolved value types are $"Or" arrow.r "Or"$.
 
@@ -18104,9 +18094,9 @@ The following table shows concrete target-variable counts for example instances,
 #reduction-rule("KSatisfiability", "FeasibleRegisterAssignment",
   example: false,
 )[
-  Sethi's Reduction 3 @sethi1973 builds a DAG with shared-register variable leaf pairs and $p\/q\/r\/overline(r)$ clause gadgets. Nonempty short clauses are padded by repeating a literal; occurring variables are compacted. For $s$ declared source variables and $c$ clauses, the target has at most $2s+12c$ vertices, $15c$ arcs, $s+9c$ registers, and $s+3c$ pairs of vertices sharing a register.
+  Sethi's Reduction 3 @sethi1973 builds a DAG with shared-register variable leaf pairs and $p\/q\/r\/overline(r)$ clause gadgets. Occurring variables are compacted. For $s$ declared source variables and $c$ clauses, the target has at most $2s+12c$ vertices, $15c$ arcs, $s+9c$ registers, and $s+3c$ pairs of vertices sharing a register.
 ][
-  _Native normalization._ If any clause is empty, return the three-vertex DAG with dependencies $(2,0),(2,1)$ and register assignment $(0,0,1)$. Both predecessors must stay live until vertex 2, so neither can overwrite the other's register; this target is infeasible. Otherwise collect appearing source indices in increasing order and store their inverse map. Pad each nonempty clause to three literal occurrences by repeating its first literal. Repetition preserves a disjunction, and each occurrence has its own gadget and register pair, so no distinct-variable assumption is needed. An empty conjunction yields the empty DAG and empty realization.
+  _Native normalization._ Collect appearing source indices in increasing order and store their inverse map. Each of the three literal occurrences of a clause, including repeated literals, has its own gadget and register pair, so no distinct-variable assumption is needed. An empty conjunction yields the empty DAG and empty realization.
 
   _Construction._ Let $a$ be the number of appearing variables. For each compact variable $x_k$, create leaves $s_k^+,s_k^-$ sharing register $S_k$. For every clause position $(i,j)$ create $p_(i,j),q_(i,j),r_(i,j),overline(r)_(i,j)$. The $p$ and $q$ registers are unique, while $r$ and $overline(r)$ share a fresh register $R_(i,j)$. Arcs point from a consumer to its dependency: $q_(i,j) -> p_(i,j) -> r_(i,j)$ and $q_(i,j) -> overline(r)_(i,j+1)$, with positions cyclic modulo three. For positive literal $x_k$, add $r_(i,j) -> s_k^+$ and $overline(r)_(i,j) -> s_k^-$; reverse these attachments for a negative literal. This DAG has four levels: leaves, $r/overline(r)$, $p$, and $q$.
 
@@ -18116,7 +18106,7 @@ The following table shows concrete target-variable counts for example instances,
 
   _Extraction._ Validate the complete position vector and reject $"Or(false)"$. Set each appearing source variable true iff its compact positive leaf occurs before its negative leaf. Restore original indices through the inverse map and assign false to unused variables. The target model's permitted last-use overwrite does not weaken the order-transfer proof: neither member of a shared pair is the other member's consumer in this construction.
 
-  _Bounds and native arithmetic._ For the ordinary construction $a <= min(s,3c)$, so the displayed upper bounds follow from the exact counts $2a+12c$, $15c$, $a+9c$, and $a+3c$. The fixed NO target has counts $(3,2,2,1)$ and also satisfies the bounds whenever an empty clause exists; the empty YES target has all counts zero. Let $I="isize::MAX"$. A native source clause stores a vector object of 24 bytes on 64-bit or 12 bytes on 32-bit, so successful allocation of its outer vector bounds $c$ by $I/24$ or $I/12$. Therefore $2a+12c <= 18c$, $a+9c <= 12c$, and $15c$ fit $"usize"$ before target allocation on both architectures. Once the target register-assignment vector is allocated, every indexed vertex is within that vector. All same-register groups have size two except the fixed target's singleton, so pair counting introduces no large product. Checked construction arithmetic is retained; allocation and solver limits are not infeasibility proofs.
+  _Bounds and native arithmetic._ For the ordinary construction $a <= min(s,3c)$, so the displayed upper bounds follow from the exact counts $2a+12c$, $15c$, $a+9c$, and $a+3c$. The empty YES target has all counts zero. Let $I="isize::MAX"$. A native source clause stores a vector object of 24 bytes on 64-bit or 12 bytes on 32-bit, so successful allocation of its outer vector bounds $c$ by $I/24$ or $I/12$. Therefore $2a+12c <= 18c$, $a+9c <= 12c$, and $15c$ fit $"usize"$ before target allocation on both architectures. Once the target register-assignment vector is allocated, every indexed vertex is within that vector. All same-register groups have size two, so pair counting introduces no large product. Checked construction arithmetic is retained; allocation and solver limits are not infeasibility proofs.
 ]
 
 #let ksat_rs = load-example("KSatisfiability", "RegisterSufficiency")
@@ -18141,9 +18131,9 @@ The following table shows concrete target-variable counts for example instances,
     *Multiplicity:* The fixture stores one canonical satisfying assignment. Different satisfying assignments can induce different valid computation orders in the target DAG.
   ],
 )[
-  Sethi's Reduction 1 and Theorem 3.11 @sethi1973 encode literal choices through register pressure. We extend the construction to the native zero-to-three-literal clause domain by truth-preserving normalization and explicit empty-formula boundaries. The original padding $b=max(2n-m,0)$ is retained.
+  Sethi's Reduction 1 and Theorem 3.11 @sethi1973 encode literal choices through register pressure. The native source has exactly three literals per clause, with repeated literals permitted. We compact appearing variables and handle the empty formula explicitly. The original padding $b=max(2n-m,0)$ is retained.
 ][
-  _Normalization._ A formula containing an empty clause is false; output a single output vertex with register bound zero. An empty conjunction is true; output the empty graph with bound zero. In every other case collect the appearing variables in increasing original-index order, map them to $1,dots,n$, and retain the inverse map. Keep the original clause order and literal occurrences. Repeat the first literal of each nonempty short clause until it has three positions. This preserves disjunction truth, gives $n,m>=1$, and never introduces a fictitious vertex for a missing literal. Let $Y_(i,j)$ denote the literal at position $j$ of clause $i$, allowing repeated literals.
+  _Normalization._ An empty conjunction is true; output the empty graph with bound zero. Otherwise collect the appearing variables in increasing original-index order, map them to $1,dots,n$, and retain the inverse map. Keep the original clause order and literal occurrences, which gives $n,m>=1$. Let $Y_(i,j)$ denote the literal at position $j$ of clause $i$, allowing repeated literals.
 
   _DAG construction._ Put $b=max(2n-m,0)$ and $K=3m+4n+1+b$. Arcs $(v,u)$ mean that $v$ depends on $u$. Create the following disjoint families, with one-based subscripts:
   $ |A|=2n+1, quad |B|=b, quad |C|=m, quad F={f_(i,j):1<=i<=m,1<=j<=3}, $
@@ -18305,13 +18295,13 @@ The following table shows concrete target-variable counts for example instances,
     *Multiplicity:* The fixture stores one canonical witness. The formula has multiple satisfying assignments; each induces at least one $k$-clique by choosing one true literal per clause.
   ],
 )[
-  Karp's literal-compatibility construction @karp1972 is extended with an anchor and, when needed, isolated padding. This keeps the same endpoint and handles both empty formulas and the shorter clauses accepted by the native `new_allow_less` API.
+  Karp's literal-compatibility construction @karp1972 is extended with an anchor vertex, so the empty formula maps to a one-vertex clique instance.
 ][
-  _Construction._ Let $m$ be the clause count and $t=sum_j |C_j|$ the actual occurrence count. Number literal vertices in clause/position order, with stored variable indices and polarities. Set $N=max(t,m)+1$, $k=m+1$, and anchor $a=t$. Connect two literal vertices iff they come from different clauses and are not opposite polarities of the same variable; then connect $a$ to all literal vertices. Any remaining vertices are isolated. Thus $1<=k<=N$, $N<=3m+1$, and the edge count is at most $9m^2+3m$.
+  _Construction._ Let $m$ be the clause count. Number the $3m$ literal occurrences in clause/position order, with stored variable indices and polarities. Set $N=3m+1$, $k=m+1$, and anchor $a=3m$. Connect two literal vertices iff they come from different clauses and are not opposite polarities of the same variable; then connect $a$ to all literal vertices. Thus $1<=k<=N$ and the edge count is at most $9m^2+3m$.
 
-  _Correctness._ A satisfying assignment selects a true occurrence from each clause; these mutually compatible vertices and the anchor form a $k$-clique. Conversely, the literal subgraph contains at most one vertex per clause in a clique, hence has clique number at most $m$. For $m>0$, any clique of size at least $k>=2$ excludes padding isolates and must contain the anchor plus one occurrence from every clause. Their polarities consistently satisfy all clauses. An empty clause prevents such a clique. For $m=0$, the target is a single anchor with $k=1$, and every source assignment satisfies the empty conjunction.
+  _Correctness._ A satisfying assignment selects a true occurrence from each clause; these mutually compatible vertices and the anchor form a $k$-clique. Conversely, the literal subgraph contains at most one vertex per clause in a clique, hence has clique number at most $m$. For $m>0$, any clique of size at least $k>=2$ must contain the anchor plus one occurrence from every clause. Their polarities consistently satisfy all clauses. For $m=0$, the target is a single anchor with $k=1$, and every source assignment satisfies the empty conjunction.
 
-  _Solution extraction._ Validate the complete target selection and its true clique predicate first. Decode the literal vertices via their stored source indices and signs, leaving unselected variables false; ignore the nonliteral anchor and padding by the defined mapping. Checked occurrence and output counts precede allocation. Formal `CNFClause::variables` supplies validated indices. Normal CLI/serde still requires exactly three literals per actual clause; native short-clause support does not change variants or serialization.
+  _Solution extraction._ Validate the complete target selection and its true clique predicate first. Decode the literal vertices via their stored source indices and signs, leaving unselected variables false; ignore the anchor by the defined mapping. Checked vertex and output counts precede allocation. Formal `CNFClause::variables` supplies validated indices.
 ]
 
 #let ksat_co = load-example("KSatisfiability", "CyclicOrdering")
@@ -18340,7 +18330,7 @@ The following table shows concrete target-variable counts for example instances,
 )[
   This reduction @galilMegiddo1977 first normalizes clauses to three distinct, globally ordered variables. With $s$ declared source variables and $c$ source clauses it produces at most $3s + 26c + 3$ elements and $40c + 2$ cyclic-order constraints. The original ten-constraint gadget is applied to the normalized formula.
 ][
-  _Normalization._ An empty clause maps to the fixed NO target on three elements with constraints $(0,1,2)$ and $(0,2,1)$. Otherwise remove repeated literals within each clause and discard clauses containing both signs of a variable. Compact the remaining appearing variables in increasing original-index order, retaining the inverse map. Replace a two-literal clause $(a or b)$ by $(a or b or u) and (a or b or not u)$ with fresh $u$. Replace a unit clause $a$ by the four clauses $(a or (plus.minus u) or (plus.minus v))$ over both independent signs, with fresh $u,v$. These conjunctions are true for every auxiliary assignment when the original clause is true and false for at least one constituent clause under every auxiliary assignment when the original clause is false. Every resulting clause has three distinct variables; order its literals by increasing variable index. If no clauses remain, use the one-element unconstrained YES target.
+  _Normalization._ Remove repeated literals within each clause and discard clauses containing both signs of a variable. Compact the remaining appearing variables in increasing original-index order, retaining the inverse map. Replace a two-literal clause $(a or b)$ by $(a or b or u) and (a or b or not u)$ with fresh $u$. Replace a unit clause $a$ by the four clauses $(a or (plus.minus u) or (plus.minus v))$ over both independent signs, with fresh $u,v$. These conjunctions are true for every auxiliary assignment when the original clause is true and false for at least one constituent clause under every auxiliary assignment when the original clause is false. Every resulting clause has three distinct variables; order its literals by increasing variable index. If no clauses remain, use the one-element unconstrained YES target.
 
   _Construction._ Let the normalized formula have $N$ variables and $M$ clauses. For each variable $x_i$, create three target elements $alpha_i, beta_i, gamma_i$. A positive literal has associated triple $(alpha_i,beta_i,gamma_i)$; a negative literal has $(alpha_i,gamma_i,beta_i)$. For each normalized clause, let its three literal triples be $(a,b,c)$, $(d,e,f)$, $(g,h,i)$ in increasing variable order. Add five fresh elements $j,k,l,m,n$ and the ten constraints
   $
@@ -18400,7 +18390,7 @@ The following table shows concrete target-variable counts for example instances,
 )[
   Ullman's reduction first builds a variable-capacity unit-task scheduling instance for 3-SAT, then pads each time slot with chained filler jobs so a fixed number of processors simulates the desired capacity profile. Because every task has length $1$, preemption is irrelevant: the resulting instance is already a valid preemptive scheduling instance whose optimal makespan is at most $T = n + 3$ iff the formula is satisfiable @ullman1975 @garey1979.
 ][
-  Short nonempty clauses are padded by repeating literals. An empty conjunction maps to one unit task with threshold 1; a formula containing an empty clause maps to the same task with threshold 0. The following construction handles the remaining instances.
+  An empty conjunction maps to one unit task with threshold 1. The following construction handles the remaining instances.
 
   _Construction._ Let $phi$ be a 3-CNF formula with variables $x_1, dots, x_n$ and clauses $C_1, dots, C_m$. Create unit jobs $x_(i,j)$ and $overline(x)_(i,j)$ for $1 <= i <= n$ and $0 <= j <= n$, plus forcing jobs $y_i, overline(y)_i$, and clause jobs $D_(r,s)$ for $1 <= r <= m$, $1 <= s <= 7$. Add chain precedences $x_(i,j) prec x_(i,j+1)$ and $overline(x)_(i,j) prec overline(x)_(i,j+1)$, and branching precedences $x_(i,i-1) prec y_i$, $overline(x)_(i,i-1) prec overline(y)_i$. Set $T = n + 3$ and slot capacities $c_0 = n$, $c_1 = 2n + 1$, $c_t = 2n + 2$ for $2 <= t <= n$, $c_(n+1) = m + n + 1$, and $c_(n+2) = 6m$.
   For each clause $C_r = (ell_1 or ell_2 or ell_3)$ and each nonzero bit pattern $b in {1, dots, 7}$, create clause job $D_(r,b)$. Its predecessors are the three chain endpoints chosen according to the bits of $b$: for literal position $k$, use the endpoint of $ell_k$ when bit $k$ is 1 and of $not ell_k$ when bit $k$ is 0. This makes exactly one clause job per clause ready one slot earlier when the clause is satisfied.
@@ -18483,7 +18473,7 @@ The following table shows concrete target-variable counts for example instances,
 
   _Solution extraction._ Validate the target partition, select precisely those vertex items sharing the label of $s$, and invoke the formal clique-to-SAT extractor. This mapping is independent of the numerical names of partition blocks.
 
-  _Overhead._ There are exactly $h+e+2$ vertices and $2h+4e$ arcs. With $m$ source clauses, $h<=3m+1$ and $e<=9m(m-1)/2+3m$, including native short or empty clauses. Thus target sizes are at most $(9m^2+3m+6)/2$ vertices and $18m^2+2$ arcs. The construction checks representability of counts and signed integer coefficients before allocating its incidence graph.
+  _Overhead._ There are exactly $h+e+2$ vertices and $2h+4e$ arcs. With $m$ source clauses, $h<=3m+1$ and $e<=9m(m-1)/2+3m$. Thus target sizes are at most $(9m^2+3m+6)/2$ vertices and $18m^2+2$ arcs. The construction checks representability of counts and signed integer coefficients before allocating its incidence graph.
 ]
 
 #let hc_bicon = load-example("HamiltonianCircuit", "BiconnectivityAugmentation")
@@ -19010,7 +19000,7 @@ The following table shows concrete target-variable counts for example instances,
 #reduction-rule("KSatisfiability", "BicliqueCover")[
   Polynomial reduction (Chandran, Issac, and Karrenbauer, IPEC 2016 @chandran_et_al:LIPIcs.IPEC.2016.11) from 3-SAT to BicliqueCover with logarithmic rank. Each appearing source variable is split into a positive/negative pair $(t_i, f_i)$, exactly-one clauses tie them to opposite truth values, and the formula is padded so that $n = 2^ell$ normalized variables admit a balanced satisfying assignment with exactly $n / 2$ true variables. The construction then assembles a bipartite gadget whose biclique cover rank equals $k_f + 2 ell + 2$ iff the (normalized) formula is satisfiable.
 ][
-  _Construction._ Let $psi$ have $n_s$ declared variables and $m_s$ clauses. The native Rust API also permits clauses of at most three literals. An empty clause maps to a single-edge, rank-zero NO target. A formula with no clauses maps to an empty, rank-zero YES target. Otherwise compact the $a$ variables that actually appear, recording their original indices, and repeat one literal in each nonempty short clause to obtain exactly three positions. Repetition preserves disjunction, and absent variables may be assigned false in the inverse map. *Normalize* this compact formula:
+  _Construction._ Let $psi$ have $n_s$ declared variables and $m_s$ three-literal clauses. A formula with no clauses maps to an empty, rank-zero YES target. Otherwise compact the $a$ variables that actually appear, recording their original indices; absent variables may be assigned false in the inverse map. *Normalize* this compact formula:
   $
     "vars:" quad     & "introduce" t_i, f_i "for each appearing" x_i "and pad to" n = 2^ell "variables" \
     "clauses:" quad  & "replace literal" x_i "by" t_i ";" not x_i "by" f_i \
@@ -19185,15 +19175,15 @@ The following table shows concrete target-variable counts for example instances,
 )[
   This reduction uses variable digons and clause three-cycles, following the kernel hardness approach of @chvatal1973. With $a$ appearing variables, $m$ clauses and $L$ literal occurrences, the target has $2a + 3m$ vertices and $2a + 3m + L$ arcs. These are bounded by $2n + 3m$ and $2n + 6m$ on the native source domain. Each occurrence has its own clause vertex; kernels may include clause vertices as well as literals.
 ][
-  _Construction._ Collect the sorted original indices $J$ of appearing variables, with $a = |J|$. For each compact variable $i$, create literal vertices $p_i, n_i$ and both digon arcs. Each native clause has zero through three literals. Create three vertices $c_(j,0), c_(j,1), c_(j,2)$ and the directed cycle in that order, then add $(c_(j,t), v(ell_(j,t)))$ only for its actual literal positions. Repeated literals keep separate occurrence vertices. An empty clause therefore produces a three-cycle with no outgoing literal arcs, which has no kernel; an empty formula produces an empty graph, whose empty selection is a kernel. No padding is needed.
+  _Construction._ Collect the sorted original indices $J$ of appearing variables, with $a = |J|$. For each compact variable $i$, create literal vertices $p_i, n_i$ and both digon arcs. For each clause create three vertices $c_(j,0), c_(j,1), c_(j,2)$ and the directed cycle in that order, then add $(c_(j,t), v(ell_(j,t)))$ for its three literal positions. Repeated literals keep separate occurrence vertices. An empty formula produces an empty graph, whose empty selection is a kernel.
 
-  _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, choose its true literal in each digon. Let $t_r$ indicate whether the literal at clause position $r$ is selected, with missing positions set to false. Select clause vertex $r$ exactly when $not t_r and t_((r+1) mod 3)$. A selected vertex points to no selected literal, and its successor cannot be selected, so independence holds. An unselected vertex with $t_r$ true is absorbed through its literal arc. Otherwise both $t_r$ and $t_((r+1) mod 3)$ are false. Since the clause is satisfied, $t_((r+2) mod 3)$ is true; its cycle successor is therefore selected and absorbs it. Unselected literal vertices are absorbed by their digon partners.
+  _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, choose its true literal in each digon. Let $t_r$ indicate whether the literal at clause position $r$ is selected. Select clause vertex $r$ exactly when $not t_r and t_((r+1) mod 3)$. A selected vertex points to no selected literal, and its successor cannot be selected, so independence holds. An unselected vertex with $t_r$ true is absorbed through its literal arc. Otherwise both $t_r$ and $t_((r+1) mod 3)$ are false. Since the clause is satisfied, $t_((r+2) mod 3)$ is true; its cycle successor is therefore selected and absorbs it. Unselected literal vertices are absorbed by their digon partners.
 
-  ($arrow.l.double$) Each literal vertex has only its digon partner as an outgoing neighbor. Independence and absorption force exactly one selected endpoint per variable. If a clause has no selected literal, absorption must occur entirely within its directed three-cycle. Independence permits at most one selected cycle vertex, which cannot absorb both others. This contradiction proves that every clause is satisfied, including the native short-clause semantics. This proof does not require distinct variables or a particular literal order.
+  ($arrow.l.double$) Each literal vertex has only its digon partner as an outgoing neighbor. Independence and absorption force exactly one selected endpoint per variable. If a clause has no selected literal, absorption must occur entirely within its directed three-cycle. Independence permits at most one selected cycle vertex, which cannot absorb both others. This contradiction proves that every clause is satisfied. This proof does not require distinct variables or a particular literal order.
 
   _Solution extraction._ Validate the target selection once using the formal target evaluator and reject $"Or(false)"$. Initialize a length-$n$ false vector and restore each original position $J_i$ from the selection of $p_i$. Unused variables remain false; selected clause vertices are ignored. The concrete value types are $"Or" arrow.r "Or"$.
 
-  _Bounds and native arithmetic._ Since $a <= L <= 3m$, the target has at most $9m$ vertices and $12m$ arcs. The registered relations use upper bounds in the declared source parameters, covering sparse variables and short clauses. Counts are checked before allocation, and every vertex index is bounded by the checked total. A successfully allocated native clause vector also bounds $m$ by its element layout and the address space; original sparse indices are never doubled. Allocation limits do not represent mathematical infeasibility.
+  _Bounds and native arithmetic._ Since $a <= L <= 3m$, the target has at most $9m$ vertices and $12m$ arcs. The registered relations use upper bounds in the declared source parameters, covering sparse variables. Counts are checked before allocation, and every vertex index is bounded by the checked total. A successfully allocated native clause vector also bounds $m$ by its element layout and the address space; original sparse indices are never doubled. Allocation limits do not represent mathematical infeasibility.
 
 ]
 
@@ -19988,15 +19978,13 @@ The following table shows concrete target-variable counts for example instances,
     *Multiplicity:* The fixture stores one canonical witness. The form is invariant under $f arrow.r -f$, so the complementary assignment $(-1, +1, -1, +1)$ (config $(0, 1, 0, 1)$) is equally optimal.
   ],
 )[
-  @garey1979 (MS13) The construction takes $A$ to be the weighted adjacency matrix of $G$. The identity $sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 dot "cut"(S)$ — where $S = {i : f(i) = +1\}$ and $W = sum_(e in E) w(e)$ — converts MaxCut maximization into MinimumMatrixCover minimization with $O(n^2)$ overhead.
+  @garey1979 (MS13) The construction takes $A$ to be the weighted adjacency matrix of $G$. The identity $sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 dot "cut"(S)$ — where $S = {i : f(i) = +1\}$ and $W = sum_(e in E) w(e)$ — converts MaxCut maximization into MinimumMatrixCover minimization with $O(n^2)$ overhead for nonnegative weights. Each negative edge first becomes a two-edge gadget through one auxiliary vertex, giving $O((n + |E|)^2)$ overhead.
 ][
-  _Construction._ Given a MaxCut instance $(G, w)$ with $G = (V, E)$, $|V| = n$, and nonnegative integer edge weights $w$, build the $n times n$ matrix $A$ with $a_(i j) = w(\{i, j\})$ for $\{i, j\} in E$, $a_(i j) = 0$ otherwise, and $a_(i i) = 0$. $A$ is symmetric, zero-diagonal, and nonnegative, hence a valid MinimumMatrixCover instance.
-
-  _Correctness._ For any $f in \{-1, +1\}^n$ with $S = \{i : f(i) = +1\}$, each edge $\{i, j\} in E$ appears twice in $sum_(i, j) a_(i j) f(i) f(j)$. A non-cut edge contributes $+2 w(\{i, j\})$ (same signs, $f(i) f(j) = +1$); a cut edge contributes $-2 w(\{i, j\})$. Summing yields $sum_(i, j) a_(i j) f(i) f(j) = 2 (W - "cut"(S)) - 2 "cut"(S) = 2 W - 4 "cut"(S)$. Since $2 W$ is a constant, $min_f sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 max_S "cut"(S)$, so the two problems share the same optimal partitions. ($arrow.r.double$) A maximum cut $S^*$ defines $f^*$ minimizing the quadratic form. ($arrow.l.double$) A minimizing $f^*$ defines $S^* = \{i : f^*(i) = +1\}$ achieving the maximum cut.
+  _Construction._ Given a MaxCut instance $(G, w)$ with $G = (V, E)$ and $|V| = n$, first remove negative weights. Replace each edge $\{u, v\}$ with $w(\{u, v\}) < 0$ by a fresh vertex $t$ and edges $\{t, v\}$ of weight $|w| + 1$ and $\{t, u\}$ of weight $|w|$. The resulting graph $G'$ has $n' <= n + |E|$ vertices and nonnegative weights $w'$. Build the $n' times n'$ matrix $A$ with $a_(i j) = w'(\{i, j\})$ for edges of $G'$, $a_(i j) = 0$ otherwise, and $a_(i i) = 0$. $A$ is symmetric, zero-diagonal, and nonnegative, hence a valid MinimumMatrixCover instance.
 
-  _Precondition._ Nonnegative edge weights. Negative-weight MaxCut instances are out of scope; a separate weight-shifting reduction would be required.
+  _Correctness._ For any $f in \{-1, +1\}^n$ with $S = \{i : f(i) = +1\}$, each edge $\{i, j\} in E$ appears twice in $sum_(i, j) a_(i j) f(i) f(j)$. A non-cut edge contributes $+2 w(\{i, j\})$ (same signs, $f(i) f(j) = +1$); a cut edge contributes $-2 w(\{i, j\})$. Summing yields $sum_(i, j) a_(i j) f(i) f(j) = 2 (W - "cut"(S)) - 2 "cut"(S) = 2 W - 4 "cut"(S)$. Since $2 W$ is a constant, $min_f sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 max_S "cut"(S)$ on $G'$. Each gadget preserves maximum cuts: moving $t$ to the side opposite $v$ gains $|w| + 1$ and loses at most $|w|$, so every maximum cut of $G'$ separates $t$ from $v$. Then $\{t, u\}$ is cut exactly when $u$ and $v$ share a side, and $|w| dot [u, v "together"] = w dot [u, v "cut"] + |w|$. Each gadget therefore adds the constant $2|w| + 1$, and maximum cuts of $G'$ restrict to maximum cuts of $G$; every maximum cut of $G$ extends to one of $G'$. Hence the two problems share the same optimal partitions on $V$. ($arrow.r.double$) A maximum cut $S^*$ defines $f^*$ minimizing the quadratic form. ($arrow.l.double$) A minimizing $f^*$ defines $S^* = \{i : f^*(i) = +1\}$ achieving the maximum cut.
 
-  _Solution extraction._ Both encodings agree that $"config"[i] = 1$ means vertex $i in S$, so extraction is the identity. The complementary witness $f arrow.r -f$ is equally optimal because the quadratic form is invariant under this sign flip.
+  _Solution extraction._ Both encodings agree that $"config"[i] = 1$ means vertex $i in S$, so extraction keeps the original vertices' bits and drops the auxiliary ones. The complementary witness $f arrow.r -f$ is equally optimal because the quadratic form is invariant under this sign flip.
 ]
 
 // 14. HamiltonianPath → IsomorphicSpanningTree (#912)
diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs
index 05edafeb9..13a3bd934 100644
--- a/problemreductions-cli/src/cli.rs
+++ b/problemreductions-cli/src/cli.rs
@@ -507,17 +507,17 @@ mod tests {
         let cli = Cli::try_parse_from([
             "pred",
             "create",
-            "3SAT",
+            "2SAT",
             "--num-vars",
             "3",
             "--clauses",
-            "1,2,3",
+            "1,2",
         ])
         .expect("variant alias parses");
         let Commands::Create(args) = cli.command else {
             panic!("expected create command");
         };
-        assert_eq!(args.problem.as_deref(), Some("KSatisfiability/K3"));
+        assert_eq!(args.problem.as_deref(), Some("KSatisfiability/K2"));
         assert_eq!(args.raw("num-vars"), Some("3"));
     }
 
diff --git a/src/models/algebraic/consecutive_ones_submatrix.rs b/src/models/algebraic/consecutive_ones_submatrix.rs
index bad2a8a4c..7cd3e6832 100644
--- a/src/models/algebraic/consecutive_ones_submatrix.rs
+++ b/src/models/algebraic/consecutive_ones_submatrix.rs
@@ -21,7 +21,7 @@ inventory::submit! {
         description: "Find K columns of a binary matrix that can be permuted to have the consecutive ones property",
         fields: &[
             FieldInfo { name: "matrix", type_name: "Vec<Vec<bool>>", description: "m×n binary matrix A" },
-            FieldInfo { name: "bound", type_name: "i64", description: "Required number of columns K" },
+            FieldInfo { name: "bound", type_name: "usize", description: "Required number of columns K" },
         ],
     }
 }
@@ -62,13 +62,13 @@ inventory::submit! {
 #[serde(try_from = "ConsecutiveOnesSubmatrixData")]
 pub struct ConsecutiveOnesSubmatrix {
     matrix: Vec<Vec<bool>>,
-    bound: i64,
+    bound: usize,
 }
 
 #[derive(Deserialize)]
 struct ConsecutiveOnesSubmatrixData {
     matrix: Vec<Vec<bool>>,
-    bound: i64,
+    bound: usize,
 }
 
 impl TryFrom<ConsecutiveOnesSubmatrixData> for ConsecutiveOnesSubmatrix {
@@ -85,19 +85,19 @@ impl ConsecutiveOnesSubmatrix {
     /// # Panics
     ///
     /// Panics if `bound > n`, or if rows have inconsistent lengths.
-    pub fn new(matrix: Vec<Vec<bool>>, bound: i64) -> Self {
+    pub fn new(matrix: Vec<Vec<bool>>, bound: usize) -> Self {
         Self::try_new(matrix, bound).unwrap_or_else(|error| panic!("{error}"))
     }
 
     fn try_new(
         matrix: Vec<Vec<bool>>,
-        bound: i64,
+        bound: usize,
     ) -> Result<Self, crate::registry::ConstructionError> {
         let n = matrix.first().map_or(0, Vec::len);
         if matrix.iter().any(|row| row.len() != n) {
             return Err("all matrix rows must have the same length".into());
         }
-        if !(bound < 0 || usize::try_from(bound).is_ok_and(|bound| bound <= n)) {
+        if bound > n {
             return Err(format!("bound ({bound}) must be <= number of columns ({n})").into());
         }
         Ok(Self { matrix, bound })
@@ -109,7 +109,7 @@ impl ConsecutiveOnesSubmatrix {
     }
 
     /// Returns the bound (the required number of columns).
-    pub fn bound(&self) -> i64 {
+    pub fn bound(&self) -> usize {
         self.bound
     }
 
@@ -222,7 +222,7 @@ impl Problem for ConsecutiveOnesSubmatrix {
                     .filter(|(_, &v)| v)
                     .map(|(i, _)| i)
                     .collect();
-                if usize::try_from(self.bound) != Ok(selected.len()) {
+                if self.bound != selected.len() {
                     return Ok(crate::types::Or(false));
                 }
                 self.any_permutation_has_c1p(&selected)
diff --git a/src/models/formula/ksat.rs b/src/models/formula/ksat.rs
index dede5be57..6d2e9bb7c 100644
--- a/src/models/formula/ksat.rs
+++ b/src/models/formula/ksat.rs
@@ -7,7 +7,7 @@
 
 use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension};
 use crate::traits::Problem;
-use crate::variant::{KValue, K2, K3, KN};
+use crate::variant::{KValue, K2, K3};
 use serde::{de::Error as _, Deserialize, Deserializer, Serialize};
 
 use super::{sat::validate_cnf_literals, CNFClause};
@@ -53,7 +53,7 @@ inventory::submit! {
         name: "KSatisfiability",
         display_name: "K-Satisfiability",
         aliases: &["KSAT"],
-        dimensions: &[VariantDimension::new("k", "KN", &["KN", "K2", "K3"])],
+        dimensions: &[VariantDimension::new("k", "K3", &["K3", "K2"])],
         category: crate::registry::ProblemCategory::Formula,
         module_path: module_path!(),
         description: "SAT with exactly k literals per clause",
@@ -124,63 +124,24 @@ impl<K: KValue> KSatisfiability<K> {
     /// Create a new K-SAT problem.
     ///
     /// # Panics
-    /// Panics if any clause does not have exactly K literals (when K is a
-    /// concrete value like K2, K3). When K is KN (arbitrary), no clause-length
-    /// validation is performed.
+    /// Panics if any clause does not have exactly K literals.
     pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
         Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
     }
 
-    /// Create a K-SAT problem after validating its clauses.
+    /// Create a K-SAT problem after validating that every clause has exactly
+    /// K literals.
     pub fn try_new(
         num_vars: usize,
         clauses: Vec<CNFClause>,
     ) -> Result<Self, crate::registry::ConstructionError> {
         validate_cnf_literals(num_vars, &clauses)?;
-        if let Some(k) = K::K {
-            for (i, clause) in clauses.iter().enumerate() {
-                if clause.len() != k {
-                    return Err(
-                        format!("Clause {i} has {} literals, expected {k}", clause.len()).into(),
-                    );
-                }
-            }
-        }
-        Ok(Self {
-            num_vars,
-            clauses,
-            _phantom: std::marker::PhantomData,
-        })
-    }
-
-    /// Create a new K-SAT problem allowing clauses with fewer than K literals.
-    ///
-    /// This is useful when the reduction algorithm produces clauses with
-    /// fewer literals (e.g., when allow_less is true in the Julia implementation).
-    ///
-    /// # Panics
-    /// Panics if any clause has more than K literals (when K is a concrete
-    /// value like K2, K3). When K is KN (arbitrary), no clause-length
-    /// validation is performed.
-    pub fn new_allow_less(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
-        Self::try_new_allow_less(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
-    }
-
-    /// Create a K-SAT problem with shorter clauses after validation.
-    pub fn try_new_allow_less(
-        num_vars: usize,
-        clauses: Vec<CNFClause>,
-    ) -> Result<Self, crate::registry::ConstructionError> {
-        validate_cnf_literals(num_vars, &clauses)?;
-        if let Some(k) = K::K {
-            for (i, clause) in clauses.iter().enumerate() {
-                if clause.len() > k {
-                    return Err(format!(
-                        "Clause {i} has {} literals, expected at most {k}",
-                        clause.len()
-                    )
-                    .into());
-                }
+        let k = K::K.ok_or("KSatisfiability requires a fixed clause width K")?;
+        for (i, clause) in clauses.iter().enumerate() {
+            if clause.len() != k {
+                return Err(
+                    format!("Clause {i} has {} literals, expected {k}", clause.len()).into(),
+                );
             }
         }
         Ok(Self {
@@ -273,13 +234,11 @@ impl<K: KValue> crate::solvers::BruteForceProblem for KSatisfiability<K> {
 }
 
 crate::declare_variants! {
-    default KSatisfiability<KN> => "2^num_vars",
+    default KSatisfiability<K3> => "1.307^num_vars" aliases ["3SAT"],
     KSatisfiability<K2> => "num_vars + num_clauses" aliases ["2SAT"],
-    KSatisfiability<K3> => "1.307^num_vars" aliases ["3SAT"],
 }
 
 crate::register_brute_force! {
-    KSatisfiability<KN> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
     KSatisfiability<K2> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
     KSatisfiability<K3> decode |_, indices: Vec<usize>| crate::config::config_to_bits(&indices),
 }
diff --git a/src/rules/biconnectivityaugmentation_ilp.rs b/src/rules/biconnectivityaugmentation_ilp.rs
index f8bc8e07f..f15484f23 100644
--- a/src/rules/biconnectivityaugmentation_ilp.rs
+++ b/src/rules/biconnectivityaugmentation_ilp.rs
@@ -81,9 +81,9 @@ impl crate::rules::AggregateReductionResult for ReductionBiconnAugToILP {}
 #[reduction(transform = {
     exact {
         max_constraint_magnitude_bits = "max_numeric_magnitude_bits",
+        num_vars = "num_potential_edges + 2 * num_vertices * (num_vertices + 1) * (num_edges + num_potential_edges)",
     },
     upper_bound {
-        num_vars = "num_potential_edges + 2 * num_vertices * (num_vertices + 1) * (num_edges + num_potential_edges)",
         num_constraints = "1 + num_vertices * (num_vertices + 1) * (2 * num_edges + 4 * num_potential_edges + num_vertices)",
         num_nonzeros = "num_potential_edges + num_vertices * (num_vertices + 1) * (4 * num_edges + 8 * num_potential_edges)",
     },
diff --git a/src/rules/clustering_ilp.rs b/src/rules/clustering_ilp.rs
index ca6434296..69bbb04af 100644
--- a/src/rules/clustering_ilp.rs
+++ b/src/rules/clustering_ilp.rs
@@ -49,11 +49,15 @@ impl ReductionResult for ReductionClusteringToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionClusteringToILP {}
 
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "1",
-    num_vars = "num_elements * num_clusters",
-    num_constraints = "num_elements + num_elements * (num_elements - 1) / 2 * num_clusters",
-    num_nonzeros = "num_elements * num_clusters + num_elements * (num_elements - 1) * num_clusters",
+#[reduction(transform = {
+    exact {
+        num_vars = "num_elements * num_clusters",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "1",
+        num_constraints = "num_elements + num_elements * (num_elements - 1) / 2 * num_clusters",
+        num_nonzeros = "num_elements * num_clusters + num_elements * (num_elements - 1) * num_clusters",
+    },
 })]
 impl ReduceTo<ILP<bool>> for Clustering {
     type Result = ReductionClusteringToILP;
diff --git a/src/rules/consecutiveblockminimization_ilp.rs b/src/rules/consecutiveblockminimization_ilp.rs
index 7ff7395b6..8ed091c3d 100644
--- a/src/rules/consecutiveblockminimization_ilp.rs
+++ b/src/rules/consecutiveblockminimization_ilp.rs
@@ -43,11 +43,15 @@ impl ReductionResult for ReductionCBMToILP {
 impl crate::rules::AggregateReductionResult for ReductionCBMToILP {}
 
 #[reduction(
-    transform = upper_bound {
-        max_constraint_magnitude_bits = "num_rows * num_cols + 1",
-        num_vars = "num_cols * num_cols + num_rows * num_cols + num_rows * num_cols",
-        num_constraints = "num_cols + num_cols + num_rows * num_cols + num_rows + num_rows * num_cols + 1",
-        num_nonzeros = "2 * num_cols^2 + num_rows * num_cols^2 + 5 * num_rows * num_cols",
+    transform = {
+        exact {
+            num_vars = "num_cols * num_cols + num_rows * num_cols + num_rows * num_cols",
+        },
+        upper_bound {
+            max_constraint_magnitude_bits = "num_rows * num_cols + 1",
+            num_constraints = "num_cols + num_cols + num_rows * num_cols + num_rows + num_rows * num_cols + 1",
+            num_nonzeros = "2 * num_cols^2 + num_rows * num_cols^2 + 5 * num_rows * num_cols",
+        },
     },
 )]
 impl ReduceTo<ILP<bool>> for ConsecutiveBlockMinimization {
diff --git a/src/rules/consecutiveonessubmatrix_ilp.rs b/src/rules/consecutiveonessubmatrix_ilp.rs
index c3db9451a..060040ce8 100644
--- a/src/rules/consecutiveonessubmatrix_ilp.rs
+++ b/src/rules/consecutiveonessubmatrix_ilp.rs
@@ -46,11 +46,15 @@ impl ReductionResult for ReductionCOSToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionCOSToILP {}
 
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "bound + num_cols + 1",
-    num_vars = "num_cols + num_cols * bound + 5 * num_rows * bound",
-    num_constraints = "2 + num_cols + bound + 3 * num_rows + 8 * num_rows * bound",
-    num_nonzeros = "2 * num_cols + 2 * num_cols * bound + num_rows * num_cols * bound + 2 * num_rows * bound^2 + 21 * num_rows * bound",
+#[reduction(transform = {
+    exact {
+        num_vars = "num_cols + num_cols * bound + 5 * num_rows * bound",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "bound + num_cols + 1",
+        num_constraints = "2 + num_cols + bound + 3 * num_rows + 8 * num_rows * bound",
+        num_nonzeros = "2 * num_cols + 2 * num_cols * bound + num_rows * num_cols * bound + 2 * num_rows * bound^2 + 21 * num_rows * bound",
+    },
 })]
 impl ReduceTo<ILP<bool>> for ConsecutiveOnesSubmatrix {
     type Result = ReductionCOSToILP;
@@ -58,7 +62,7 @@ impl ReduceTo<ILP<bool>> for ConsecutiveOnesSubmatrix {
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
         let m = self.num_rows();
         let n = self.num_cols();
-        let k = self.bound() as usize;
+        let k = self.bound();
 
         // Variable layout (all binary):
         // s_c: n vars at [0, n)  — column selection
diff --git a/src/rules/directedhamiltonianpath_ilp.rs b/src/rules/directedhamiltonianpath_ilp.rs
index c5c821c84..133efcf35 100644
--- a/src/rules/directedhamiltonianpath_ilp.rs
+++ b/src/rules/directedhamiltonianpath_ilp.rs
@@ -53,11 +53,15 @@ impl ReductionResult for ReductionDirectedHamiltonianPathToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionDirectedHamiltonianPathToILP {}
 
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "1",
-    num_vars = "num_vertices^2",
-    num_constraints = "3 * num_vertices + num_vertices^3",
-    num_nonzeros = "num_vertices^2 + 2 * num_vertices^3",
+#[reduction(transform = {
+    exact {
+        num_vars = "num_vertices^2",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "1",
+        num_constraints = "3 * num_vertices + num_vertices^3",
+        num_nonzeros = "num_vertices^2 + 2 * num_vertices^3",
+    },
 })]
 impl ReduceTo<ILP<bool>> for DirectedHamiltonianPath {
     type Result = ReductionDirectedHamiltonianPathToILP;
diff --git a/src/rules/directedtwocommodityintegralflow_ilp.rs b/src/rules/directedtwocommodityintegralflow_ilp.rs
index f08d07b2f..edf1a5c29 100644
--- a/src/rules/directedtwocommodityintegralflow_ilp.rs
+++ b/src/rules/directedtwocommodityintegralflow_ilp.rs
@@ -56,11 +56,15 @@ impl ReductionResult for ReductionD2CIFToILP {
 impl crate::rules::AggregateReductionResult for ReductionD2CIFToILP {}
 
 #[reduction(
-    transform = upper_bound {
-        max_constraint_magnitude_bits = "max_capacity * (num_arcs + 1) + 2",
-        num_vars = "2 * num_arcs",
-        num_constraints = "num_arcs + 2 * num_vertices + 2",
-        num_nonzeros = "(2 * num_arcs) * (num_arcs + 2 * num_vertices + 2)",
+    transform = {
+        exact {
+            num_vars = "2 * num_arcs",
+        },
+        upper_bound {
+            max_constraint_magnitude_bits = "max_capacity * (num_arcs + 1) + 2",
+            num_constraints = "num_arcs + 2 * num_vertices + 2",
+            num_nonzeros = "(2 * num_arcs) * (num_arcs + 2 * num_vertices + 2)",
+        },
     },
 )]
 impl ReduceTo<ILP<i64, i64, Bounded>> for DirectedTwoCommodityIntegralFlow {
diff --git a/src/rules/flowshopscheduling_ilp.rs b/src/rules/flowshopscheduling_ilp.rs
index 6845717cd..2a85d956a 100644
--- a/src/rules/flowshopscheduling_ilp.rs
+++ b/src/rules/flowshopscheduling_ilp.rs
@@ -72,11 +72,15 @@ impl ReductionResult for ReductionFSSToILP {
 impl crate::rules::AggregateReductionResult for ReductionFSSToILP {}
 
 #[reduction(
-    transform = upper_bound {
-        max_constraint_magnitude_bits = "max_time_bits + 1",
-        num_vars = "num_jobs * (num_jobs - 1) / 2 + num_jobs * num_processors",
-        num_constraints = "num_jobs * (num_jobs - 1) + num_jobs + num_jobs * (num_processors - 1) + num_jobs * (num_jobs - 1) * num_processors + num_jobs",
-        num_nonzeros = "num_jobs * (num_jobs - 1) * (1 + 3 * num_processors) + 2 * num_jobs * num_processors",
+    transform = {
+        exact {
+            num_vars = "num_jobs * (num_jobs - 1) / 2 + num_jobs * num_processors",
+        },
+        upper_bound {
+            max_constraint_magnitude_bits = "max_time_bits + 1",
+            num_constraints = "num_jobs * (num_jobs - 1) + num_jobs + num_jobs * (num_processors - 1) + num_jobs * (num_jobs - 1) * num_processors + num_jobs",
+            num_nonzeros = "num_jobs * (num_jobs - 1) * (1 + 3 * num_processors) + 2 * num_jobs * num_processors",
+        },
     },
 )]
 impl ReduceTo<ILP<i64, i64, Bounded>> for FlowShopScheduling {
diff --git a/src/rules/hamiltoniancircuit_ilp.rs b/src/rules/hamiltoniancircuit_ilp.rs
index c7b46ff5c..013e42d60 100644
--- a/src/rules/hamiltoniancircuit_ilp.rs
+++ b/src/rules/hamiltoniancircuit_ilp.rs
@@ -39,11 +39,15 @@ impl ReductionResult for ReductionHamiltonianCircuitToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionHamiltonianCircuitToILP {}
 
-#[crate::reduction(transform = upper_bound {
-    num_vars = "3 * num_edges",
-    num_constraints = "2 * num_vertices + 2 * num_edges + 1",
-    num_nonzeros = "10 * num_edges",
-    max_constraint_magnitude_bits = "num_vertices + 2",
+#[crate::reduction(transform = {
+    exact {
+        num_vars = "3 * num_edges",
+        num_nonzeros = "10 * num_edges",
+    },
+    upper_bound {
+        num_constraints = "2 * num_vertices + 2 * num_edges + 1",
+        max_constraint_magnitude_bits = "num_vertices + 2",
+    },
 })]
 impl ReduceTo<ILP<i64, i64, Bounded>> for HamiltonianCircuit<SimpleGraph> {
     type Result = ReductionHamiltonianCircuitToILP;
diff --git a/src/rules/isomorphicspanningtree_ilp.rs b/src/rules/isomorphicspanningtree_ilp.rs
index 6904c4be4..74e22a5c0 100644
--- a/src/rules/isomorphicspanningtree_ilp.rs
+++ b/src/rules/isomorphicspanningtree_ilp.rs
@@ -45,11 +45,15 @@ impl crate::rules::AggregateReductionResult for ReductionISTToILP {}
 // Two assignment families contribute 2n rows and 2n^2 terms. Each of the
 // n-1 tree edges emits one two-term row per ordered non-edge, at most n(n-1).
 // At n=0 both products vanish, including the otherwise negative n-1 factor.
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "2",
-    num_vars = "num_vertices * num_vertices",
-    num_constraints = "2 * num_vertices + num_vertices * (num_vertices - 1)^2",
-    num_nonzeros = "2 * num_vertices^2 + 2 * num_vertices * (num_vertices - 1)^2",
+#[reduction(transform = {
+    exact {
+        num_vars = "num_vertices * num_vertices",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "2",
+        num_constraints = "2 * num_vertices + num_vertices * (num_vertices - 1)^2",
+        num_nonzeros = "2 * num_vertices^2 + 2 * num_vertices * (num_vertices - 1)^2",
+    },
 })]
 impl ReduceTo<ILP<bool>> for IsomorphicSpanningTree<SimpleGraph> {
     type Result = ReductionISTToILP;
diff --git a/src/rules/kclique_balancedcompletebipartitesubgraph.rs b/src/rules/kclique_balancedcompletebipartitesubgraph.rs
index b3cb09b81..d2b2d330e 100644
--- a/src/rules/kclique_balancedcompletebipartitesubgraph.rs
+++ b/src/rules/kclique_balancedcompletebipartitesubgraph.rs
@@ -56,7 +56,7 @@ impl ReductionResult for ReductionKCliqueToBCBS {
 #[crate::aggregate_reduction(identity)]
 impl crate::rules::AggregateReductionResult for ReductionKCliqueToBCBS {}
 
-#[reduction(transform = upper_bound {
+#[reduction(transform = exact {
     left_size = "num_vertices + k * (k - 1) / 2",
     right_size = "num_edges + num_vertices - k",
     k = "num_vertices + k * (k - 1) / 2 - k",
diff --git a/src/rules/kernel_ilp.rs b/src/rules/kernel_ilp.rs
index 95c986253..8363af39a 100644
--- a/src/rules/kernel_ilp.rs
+++ b/src/rules/kernel_ilp.rs
@@ -36,9 +36,9 @@ impl crate::rules::AggregateReductionResult for ReductionKernelToILP {}
     exact {
         num_vars = "num_vertices",
         num_constraints = "num_arcs + num_vertices",
+        num_nonzeros = "3 * num_arcs + num_vertices",
     },
     upper_bound {
-        num_nonzeros = "3 * num_arcs + num_vertices",
         max_constraint_magnitude_bits = "2",
     },
 })]
diff --git a/src/rules/ksatisfiability_bicliquecover.rs b/src/rules/ksatisfiability_bicliquecover.rs
index dec116ab8..b26e9f457 100644
--- a/src/rules/ksatisfiability_bicliquecover.rs
+++ b/src/rules/ksatisfiability_bicliquecover.rs
@@ -5,8 +5,7 @@
 //!
 //! 1. **Normalize** the source 3-CNF formula:
 //!    - Compact the variables appearing in clauses, retaining the inverse map.
-//!      Repeat literals to pad nonempty short clauses to three positions.
-//!      Empty formulas and empty clauses map to fixed YES and NO targets.
+//!      The empty formula maps to a fixed YES target.
 //!    - For each appearing variable `x_i`, create two normalized variables
 //!      `t_i` and `f_i`. Replace literal `x_i` by `t_i`, replace literal
 //!      `¬x_i` by `f_i`. Add exactly-one clauses
@@ -205,9 +204,6 @@ fn normalize(
                 translated.push(f_lit(compact)?);
             }
         }
-        // Nonempty short clauses are equivalent after repeating a literal.
-        // Empty clauses are handled by the fixed NO construction before here.
-        translated.resize(3, translated[0]);
         clauses.push(translated);
     }
 
@@ -233,7 +229,7 @@ fn free_edge_budget(ell: usize, m: usize) -> Option<usize> {
 // With s source variables and m source clauses, the normalized counts
 // satisfy n <= 4(s+1), M <= m+4(s+1), ell <= s+1, ceil(log2 M) <= M.
 // Hence each partition is <= 31s+5m+39 and rank <= 14s+2m+22.
-// The declared coarser bounds also cover the fixed YES and NO targets.
+// The declared coarser bounds also cover the fixed YES target.
 #[crate::aggregate_reduction]
 impl crate::rules::AggregateReductionResult for ReductionKSatisfiabilityToBicliqueCover {
     type Source = KSatisfiability<K3>;
@@ -261,21 +257,10 @@ impl ReduceTo<BicliqueCover> for KSatisfiability<K3> {
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
         // ---------------- Stage 1: normalize ----------------
         let source_num_vars = self.num_vars();
-        let has_empty_clause = self
-            .clauses()
-            .iter()
-            .any(|clause| clause.literals.is_empty());
-        if has_empty_clause || self.clauses().is_empty() {
-            // The empty conjunction is YES; a conjunction with an empty
-            // disjunction is NO. Zero bicliques cover only the empty graph.
-            let size = usize::from(has_empty_clause);
-            let edges = if has_empty_clause {
-                vec![(0, 0)]
-            } else {
-                vec![]
-            };
+        if self.clauses().is_empty() {
+            // The empty conjunction is YES: zero bicliques cover the empty graph.
             return Ok(ReductionKSatisfiabilityToBicliqueCover {
-                target: BicliqueCover::new(BipartiteGraph::new(size, size, edges), 0),
+                target: BicliqueCover::new(BipartiteGraph::new(0, 0, vec![]), 0),
                 source_num_vars,
                 normalized_n: 0,
                 s1_left_offset: 0,
diff --git a/src/rules/ksatisfiability_casts.rs b/src/rules/ksatisfiability_casts.rs
deleted file mode 100644
index 898c324fa..000000000
--- a/src/rules/ksatisfiability_casts.rs
+++ /dev/null
@@ -1,26 +0,0 @@
-//! Variant reductions for KSatisfiability.
-
-use crate::impl_variant_reduction;
-use crate::models::formula::KSatisfiability;
-use crate::variant::{K2, K3, KN};
-
-impl_variant_reduction!(
-    KSatisfiability,
-    <K2> => <KN>,
-    fields: [num_vars, num_clauses, num_literals],
-    |src| KSatisfiability::new_allow_less(src.num_vars(), src.clauses().to_vec())
-);
-
-impl_variant_reduction!(
-    KSatisfiability,
-    <K3> => <KN>,
-    fields: [num_vars, num_clauses, num_literals],
-    |src| KSatisfiability::new_allow_less(src.num_vars(), src.clauses().to_vec())
-);
-
-crate::register_aggregate_reduction!(
-    crate::rules::VariantReductionResult<KSatisfiability<K2>, KSatisfiability<KN>>
-);
-crate::register_aggregate_reduction!(
-    crate::rules::VariantReductionResult<KSatisfiability<K3>, KSatisfiability<KN>>
-);
diff --git a/src/rules/ksatisfiability_cyclicordering.rs b/src/rules/ksatisfiability_cyclicordering.rs
index 313728a7e..0c2115133 100644
--- a/src/rules/ksatisfiability_cyclicordering.rs
+++ b/src/rules/ksatisfiability_cyclicordering.rs
@@ -9,10 +9,11 @@
 //! "true" one.
 //!
 //! Before applying the gadget, remove tautologies and repeated literals,
-//! compact occurring variables, and expand short clauses with fresh variables.
-//! Each resulting clause has three distinct variables in global index order.
-//! This is the hypothesis needed to combine the paper's local cyclic orders.
-//! Empty clauses and empty conjunctions map to fixed NO and YES targets.
+//! compact occurring variables, and expand clauses left with fewer than three
+//! distinct literals using fresh variables. Each resulting clause has three
+//! distinct variables in global index order. This is the hypothesis needed to
+//! combine the paper's local cyclic orders. The empty conjunction maps to a
+//! fixed YES target.
 //!
 //! Reference: Galil and Megiddo, "Cyclic ordering is NP-complete", 1977.
 
@@ -135,21 +136,17 @@ fn normalize(
                 }
             })
             .collect();
-        match *literals.as_slice() {
-            [a, b, c] => normalized.push([a, b, c]),
-            [a, b] => {
-                let u = variables.allocate()
-                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
-                normalized.extend([[a, b, u], [a, b, -u]]);
-            }
-            [a] => {
-                let u = variables.allocate()
-                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
-                let v = variables.allocate()
-                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
+        // Deduplication leaves one to three literals; fill the rest with fresh variables.
+        let fresh = variables
+            .allocate_many(3 - literals.len())
+            .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
+        match (literals.as_slice(), fresh.as_slice()) {
+            (&[a, b, c], []) => normalized.push([a, b, c]),
+            (&[a, b], &[u]) => normalized.extend([[a, b, u], [a, b, -u]]),
+            (&[a], &[u, v]) => {
                 normalized.extend([[a, u, v], [a, u, -v], [a, -u, v], [a, -u, -v]]);
             }
-            _ => unreachable!("empty clauses are handled before normalization; native clauses have at most three literals"),
+            _ => unreachable!("deduplicated three-literal clauses keep one to three literals"),
         }
     }
     // Original compact indices precede all fresh indices. Every emitted
@@ -174,18 +171,6 @@ impl ReduceTo<CyclicOrdering> for KSatisfiability<K3> {
     type Result = Reduction3SATToCyclicOrdering;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        if self
-            .clauses()
-            .iter()
-            .any(|clause| clause.literals.is_empty())
-        {
-            return Ok(Reduction3SATToCyclicOrdering {
-                target: CyclicOrdering::try_new(3, vec![(0, 1, 2), (0, 2, 1)])
-                    .map_err(<Self as ReduceTo<CyclicOrdering>>::target_construction)?,
-                source_num_vars: self.num_vars(),
-                source_variables: Vec::new(),
-            });
-        }
         let normalized = normalize(self)?;
         let num_vars = normalized.num_vars;
         let num_clauses = normalized.clauses.len();
diff --git a/src/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/rules/ksatisfiability_decisionminimumvertexcover.rs
index 7d2019231..ec37318f2 100644
--- a/src/rules/ksatisfiability_decisionminimumvertexcover.rs
+++ b/src/rules/ksatisfiability_decisionminimumvertexcover.rs
@@ -68,9 +68,9 @@ impl ReductionResult for Reduction3SATToDecisionMVC {
 impl crate::rules::AggregateReductionResult for Reduction3SATToDecisionMVC {}
 
 #[reduction(
-    transform = {
-        exact { num_vertices = "2 * num_vars + 3 * num_clauses" },
-        upper_bound { num_edges = "num_vars + 6 * num_clauses" },
+    transform = exact {
+        num_vertices = "2 * num_vars + 3 * num_clauses",
+        num_edges = "num_vars + 6 * num_clauses",
     }
 )]
 impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>> for KSatisfiability<K3> {
@@ -99,12 +99,7 @@ impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>> for KSatisfiabilit
             edges.push((base, base + 2));
 
             // Communication edges: connect triangle vertex k to the literal vertex
-            for k in 0..3 {
-                if clause.literals.is_empty() {
-                    continue;
-                }
-                // Repeating a literal pads a short clause without changing it.
-                let lit = clause.literals[k % clause.literals.len()];
+            for (k, &lit) in clause.literals.iter().enumerate() {
                 let var_idx = lit.unsigned_abs() as usize - 1; // 0-indexed variable
                 let literal_vertex = if lit > 0 {
                     2 * var_idx // positive literal vertex
@@ -122,18 +117,10 @@ impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>> for KSatisfiabilit
         Ok(Reduction3SATToDecisionMVC {
             target: Decision::new(
                 target,
-                if self
-                    .clauses()
-                    .iter()
-                    .any(|clause| clause.literals.is_empty())
-                {
-                    -1 // No nonnegative vertex-cover size can satisfy an empty clause.
-                } else {
-                    <Self as ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>>>::exact_i64(
-                        n + 2 * m,
-                        "computing the cover bound",
-                    )?
-                },
+                <Self as ReduceTo<Decision<MinimumVertexCover<SimpleGraph, One>>>>::exact_i64(
+                    n + 2 * m,
+                    "computing the cover bound",
+                )?,
             ),
             source_num_vars: n,
         })
diff --git a/src/rules/ksatisfiability_feasibleregisterassignment.rs b/src/rules/ksatisfiability_feasibleregisterassignment.rs
index c7e20a609..f4ed96f3b 100644
--- a/src/rules/ksatisfiability_feasibleregisterassignment.rs
+++ b/src/rules/ksatisfiability_feasibleregisterassignment.rs
@@ -1,9 +1,8 @@
 //! Reduction from KSatisfiability (3-SAT) to Feasible Register Assignment.
 //!
 //! This follows Sethi's Reduction 3 / Theorem 5.11 (STOC 1973):
-//! Nonempty short clauses are padded by literal repetition, an empty clause
-//! maps to a fixed infeasible DAG, and appearing variables are compacted with
-//! an inverse map. No ordering or distinct-variable hypothesis is needed.
+//! Appearing variables are compacted with an inverse map. No ordering or
+//! distinct-variable hypothesis is needed.
 //! - Variable leaf pairs `s_pos[k], s_neg[k]` share register `S[k]`
 //! - Each literal occurrence adds `p[i,j], q[i,j], r[i,j], rbar[i,j]`
 //! - `r[i,j]` and `rbar[i,j]` share register `R[i,j]`
@@ -109,19 +108,6 @@ impl ReduceTo<FeasibleRegisterAssignment> for KSatisfiability<K3> {
     type Result = Reduction3SATToFeasibleRegisterAssignment;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        if self
-            .clauses()
-            .iter()
-            .any(|clause| clause.literals.is_empty())
-        {
-            // Both predecessors must remain live until vertex 2, but they
-            // share a register. This acyclic target has no realization.
-            return Ok(Reduction3SATToFeasibleRegisterAssignment {
-                target: FeasibleRegisterAssignment::new(3, vec![(2, 0), (2, 1)], 2, vec![0, 0, 1]),
-                num_vars: self.num_vars(),
-                source_variables: Vec::new(),
-            });
-        }
         let source_variables: Vec<_> = self
             .clauses()
             .iter()
@@ -166,10 +152,9 @@ impl ReduceTo<FeasibleRegisterAssignment> for KSatisfiability<K3> {
         }
 
         for (clause_idx, clause) in self.clauses().iter().enumerate() {
-            // Repetition preserves a nonempty disjunction. Every occurrence
-            // keeps its own gadget and register pair, even for repeated literals.
-            let mut literals = clause.literals.clone();
-            literals.resize(3, literals[0]);
+            // Every occurrence keeps its own gadget and register pair, even
+            // for repeated literals.
+            let literals = &clause.literals;
             for literal_pos in 0..3 {
                 assignment[p_idx(num_vars, clause_idx, literal_pos)] =
                     p_register(num_vars, clause_idx, literal_pos);
diff --git a/src/rules/ksatisfiability_kclique.rs b/src/rules/ksatisfiability_kclique.rs
index 79dc24313..ceec31431 100644
--- a/src/rules/ksatisfiability_kclique.rs
+++ b/src/rules/ksatisfiability_kclique.rs
@@ -1,10 +1,8 @@
 //! Karp's literal-compatibility construction with a universal vertex.
 //!
-//! Use actual literal occurrences, including shorter clauses accepted by
-//! KSatisfiability::new_allow_less. For m clauses and t occurrences, create
-//! max(t,m)+1 vertices and request a clique of size m+1. Vertex t is adjacent
-//! to all literal vertices; remaining padding vertices are isolated. This
-//! uniformly represents empty formulas and formulas containing empty clauses.
+//! For m clauses, create one vertex per literal occurrence plus an anchor
+//! (3m+1 vertices) and request a clique of size m+1. The anchor is adjacent to
+//! every literal vertex, so the empty formula maps to the one-vertex clique.
 
 use crate::models::formula::KSatisfiability;
 use crate::models::graph::KClique;
@@ -57,18 +55,19 @@ impl ReductionResult for Reduction3SATToKClique {
 impl crate::rules::AggregateReductionResult for Reduction3SATToKClique {}
 
 #[reduction(
-    transform = upper_bound {
-        num_vertices = "3 * num_clauses + 1",
-        k = "num_clauses + 1",
-        num_edges = "9 * num_clauses^2 + 3 * num_clauses",
+    transform = {
+        exact {
+            k = "num_clauses + 1",
+            num_vertices = "3 * num_clauses + 1",
+        },
+        upper_bound { num_edges = "9 * num_clauses^2 + 3 * num_clauses" },
     }
 )]
 impl ReduceTo<KClique<SimpleGraph>> for KSatisfiability<K3> {
     type Result = Reduction3SATToKClique;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        let (num_vertices, k) =
-            clique_sizes(self.num_clauses(), self.clauses().iter().map(|c| c.len()))?;
+        let (num_vertices, k) = clique_sizes(self.num_clauses())?;
         // CNFClause::variables performs the formal literal-to-index conversion;
         // the source constructor has already validated its range and polarity.
         let positions: Vec<_> = self
@@ -101,22 +100,18 @@ impl ReduceTo<KClique<SimpleGraph>> for KSatisfiability<K3> {
     }
 }
 
-/// Check occurrence and output counts before allocating the compatibility graph.
-fn clique_sizes(
-    m: usize,
-    lengths: impl IntoIterator<Item = usize>,
-) -> Result<(usize, usize), crate::rules::ReductionError> {
-    let overflow = || {
-        crate::rules::ReductionError::integer_overflow::<KSatisfiability<K3>, KClique<SimpleGraph>>(
-            "counting SAT clique occurrences and auxiliary vertices",
-        )
-    };
-    let t = lengths
-        .into_iter()
-        .try_fold(0usize, |sum, len| sum.checked_add(len))
-        .ok_or_else(overflow)?;
-    let vertices = t.max(m).checked_add(1).ok_or_else(overflow)?;
-    // m+1 <= max(t,m)+1, whose representability was checked above.
+/// Check the vertex and clique sizes before allocating the compatibility graph.
+fn clique_sizes(m: usize) -> Result<(usize, usize), crate::rules::ReductionError> {
+    let vertices = m
+        .checked_mul(3)
+        .and_then(|t| t.checked_add(1))
+        .ok_or_else(|| {
+            crate::rules::ReductionError::integer_overflow::<
+                KSatisfiability<K3>,
+                KClique<SimpleGraph>,
+            >("counting SAT clique literal and anchor vertices")
+        })?;
+    // m+1 <= 3m+1, whose representability was checked above.
     Ok((vertices, m + 1))
 }
 
diff --git a/src/rules/ksatisfiability_kernel.rs b/src/rules/ksatisfiability_kernel.rs
index cef509831..2c3c1dc44 100644
--- a/src/rules/ksatisfiability_kernel.rs
+++ b/src/rules/ksatisfiability_kernel.rs
@@ -2,8 +2,8 @@
 //!
 //! This is Chvatal's 1973 construction using variable digons and clause
 //! 3-cycles with arcs to literal vertices. Appearing variables are compacted
-//! with an inverse map; native clauses of length zero through three keep
-//! their original occurrence arcs, including the empty clause's kernel-free cycle.
+//! with an inverse map; each clause keeps its three occurrence arcs, including
+//! repeated literals.
 
 use crate::models::formula::KSatisfiability;
 use crate::models::graph::Kernel;
diff --git a/src/rules/ksatisfiability_monochromatictriangle.rs b/src/rules/ksatisfiability_monochromatictriangle.rs
index d1c16cfcd..0af0eaba6 100644
--- a/src/rules/ksatisfiability_monochromatictriangle.rs
+++ b/src/rules/ksatisfiability_monochromatictriangle.rs
@@ -74,7 +74,7 @@ impl ReductionResult for Reduction3SATToMonochromaticTriangle {
 impl crate::rules::AggregateReductionResult for Reduction3SATToMonochromaticTriangle {}
 
 #[reduction(
-    transform = upper_bound {
+    transform = exact {
         num_vertices = "16 * num_vars + 40 * num_clauses + 16",
         num_edges = "50 * num_vars + 146 * num_clauses + 50",
         num_triangles = "58 * num_vars + 174 * num_clauses + 58",
@@ -87,7 +87,8 @@ impl ReduceTo<MonochromaticTriangle<SimpleGraph>> for KSatisfiability<K3> {
         let sat = ReduceTo::<Satisfiability>::reduce_to(self)?;
         let nae_reduction = ReduceTo::<NAESatisfiability>::reduce_to(sat.target_problem())?;
         let nae = nae_reduction.target_problem();
-        let auxiliary_count = nae.clauses().iter().filter(|c| c.len() == 4).count();
+        // SAT -> NAE appends the sentinel to every three-literal clause.
+        let auxiliary_count = nae.num_clauses();
         let overflow = || {
             crate::rules::ReductionError::integer_overflow::<Self, MonochromaticTriangle<SimpleGraph>>(
                 "computing signal-sender graph size",
@@ -124,21 +125,16 @@ impl ReduceTo<MonochromaticTriangle<SimpleGraph>> for KSatisfiability<K3> {
             triples.push([literal, literal, -literal]);
         }
         for clause in nae.clauses() {
-            let literals = &clause.literals;
-            if literals.len() == 4 {
-                let z = variables.allocate().map_err(
-                    crate::rules::ReductionError::construction::<
-                        Self,
-                        MonochromaticTriangle<SimpleGraph>,
-                    >,
-                )?;
-                triples.push([literals[0], literals[1], z]);
-                triples.push([-z, literals[2], literals[3]]);
-            } else {
-                // NAE(a,b) = NAE(a,b,b). Formal SAT -> NAE produces only
-                // lengths 2, 3 and 4, including NAE(s,s) for an empty clause.
-                triples.push([literals[0], literals[1], literals[literals.len() - 1]]);
-            }
+            let [a, b, c, d] = <[i64; 4]>::try_from(clause.literals.as_slice())
+                .expect("SAT -> NAE maps each three-literal clause to four literals");
+            let z = variables.allocate().map_err(
+                crate::rules::ReductionError::construction::<
+                    Self,
+                    MonochromaticTriangle<SimpleGraph>,
+                >,
+            )?;
+            triples.push([a, b, z]);
+            triples.push([-z, c, d]);
         }
 
         let mut edges = Vec::with_capacity(num_edges);
diff --git a/src/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/rules/ksatisfiability_oneinthreesatisfiability.rs
index 711f2f42c..39e6922b1 100644
--- a/src/rules/ksatisfiability_oneinthreesatisfiability.rs
+++ b/src/rules/ksatisfiability_oneinthreesatisfiability.rs
@@ -1,9 +1,8 @@
 //! Reduction from KSatisfiability (3-SAT) to One-In-Three Satisfiability.
 //!
 //! Schaefer's Lemma 3.5 (STOC 1978) expresses a three-input disjunction
-//! using five one-in-three constraints. Missing native clause positions
-//! use the forced false variable; appearing source variables are compacted
-//! and restored through an inverse map during extraction.
+//! using five one-in-three constraints. Appearing source variables are
+//! compacted and restored through an inverse map during extraction.
 
 use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability};
 use crate::reduction;
@@ -49,10 +48,15 @@ impl ReductionResult for Reduction3SATToOneInThreeSAT {
 impl crate::rules::AggregateReductionResult for Reduction3SATToOneInThreeSAT {}
 
 #[reduction(
-    transform = upper_bound {
-        num_vars = "num_vars + 2 + 6 * num_clauses",
-        num_clauses = "1 + 5 * num_clauses",
-    })]
+    transform = {
+        exact {
+            num_clauses = "1 + 5 * num_clauses",
+        },
+        upper_bound {
+            num_vars = "num_vars + 2 + 6 * num_clauses",
+        },
+    }
+)]
 impl ReduceTo<OneInThreeSatisfiability> for KSatisfiability<K3> {
     type Result = Reduction3SATToOneInThreeSAT;
 
@@ -101,9 +105,7 @@ impl ReduceTo<OneInThreeSatisfiability> for KSatisfiability<K3> {
         clauses.push(CNFClause::new(vec![z_false, z_false, z_true]));
 
         for clause in self.clauses() {
-            // Adding false disjuncts preserves every native clause, including
-            // the empty disjunction, while using the same three-input gadget.
-            let mut literals = [z_false; 3];
+            let mut literals = [0; 3];
             for (position, &literal) in clause.literals.iter().enumerate() {
                 let original = usize::try_from(literal.unsigned_abs())
                     .expect("native SAT indices fit usize")
diff --git a/src/rules/ksatisfiability_preemptivescheduling.rs b/src/rules/ksatisfiability_preemptivescheduling.rs
index c3d799ced..7d3291e2f 100644
--- a/src/rules/ksatisfiability_preemptivescheduling.rs
+++ b/src/rules/ksatisfiability_preemptivescheduling.rs
@@ -4,8 +4,8 @@
 //! scheduling instance. Since every task has length 1, preemption is inert:
 //! the constructed instance is a valid preemptive scheduling problem whose
 //! optimal makespan hits the threshold `T = num_vars + 3` iff a nontrivial
-//! 3-SAT instance is satisfiable. Empty formulas and empty clauses use a
-//! one-task instance with bound 1 and 0 respectively.
+//! 3-SAT instance is satisfiable. The empty formula uses a one-task instance
+//! with bound 1.
 //!
 //! Reference: Jeffrey D. Ullman, "NP-complete scheduling problems", JCSS 10,
 //! 1975; Garey & Johnson, Appendix A5.2.
@@ -147,8 +147,7 @@ fn build_ullman_construction(source: &KSatisfiability<K3>) -> UllmanConstruction
     for (clause_index, clause) in source.clauses().iter().enumerate() {
         for (pattern_index, &clause_job) in clause_jobs[clause_index].iter().enumerate() {
             let pattern = pattern_index + 1;
-            // Repeating literals preserves shorter nonempty disjunctions.
-            for (position, &literal) in clause.literals.iter().cycle().take(3).enumerate() {
+            for (position, &literal) in clause.literals.iter().enumerate() {
                 let bit_is_one = ((pattern >> (2 - position)) & 1) == 1;
                 precedences.push((
                     literal_endpoint(
@@ -202,7 +201,7 @@ fn clause_pattern_for_assignment(
     assignment: &[bool],
 ) -> usize {
     let mut pattern = 0usize;
-    for (position, &literal) in clause.literals.iter().cycle().take(3).enumerate() {
+    for (position, &literal) in clause.literals.iter().enumerate() {
         let variable = literal.unsigned_abs() as usize - 1;
         let value = assignment[variable];
         let literal_true = if literal > 0 { value } else { !value };
@@ -219,11 +218,8 @@ fn construct_schedule_from_assignment(
     assignment: &[bool],
     source: &KSatisfiability<K3>,
 ) -> Option<Vec<Vec<bool>>> {
-    if source.num_clauses() == 0 || source.clauses().iter().any(|c| c.literals.is_empty()) {
-        return crate::traits::Problem::evaluate(source, &assignment.to_vec())
-            .unwrap()
-            .0
-            .then(|| vec![vec![true]]);
+    if source.num_clauses() == 0 {
+        return (assignment.len() == source.num_vars()).then(|| vec![vec![true]]);
     }
     let construction = build_ullman_construction(source);
     if assignment.len() != source.num_vars() || target.num_tasks() != construction.num_jobs {
@@ -383,14 +379,13 @@ impl ReduceTo<PreemptiveScheduling> for KSatisfiability<K3> {
     type Result = Reduction3SATToPreemptiveScheduling;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        let has_empty_clause = self.clauses().iter().any(|c| c.literals.is_empty());
-        if self.num_clauses() == 0 || has_empty_clause {
-            // A one-task schedule meets bound 1, but cannot meet bound 0.
+        if self.num_clauses() == 0 {
+            // The empty conjunction is YES: a one-task schedule meets bound 1.
             return Ok(Reduction3SATToPreemptiveScheduling {
                 target: PreemptiveScheduling::new(vec![1], 1, vec![])
                     .map_err(<Self as ReduceTo<PreemptiveScheduling>>::target_construction)?,
                 positive_start_jobs: vec![0; self.num_vars()],
-                threshold: usize::from(!has_empty_clause),
+                threshold: 1,
             });
         }
         let construction = build_ullman_construction(self);
diff --git a/src/rules/ksatisfiability_quadraticcongruences.rs b/src/rules/ksatisfiability_quadraticcongruences.rs
index 74680d9b8..585b7fdd4 100644
--- a/src/rules/ksatisfiability_quadraticcongruences.rs
+++ b/src/rules/ksatisfiability_quadraticcongruences.rs
@@ -2,8 +2,8 @@
 //!
 //! Manders and Adleman (ERL-M615, 1976), Section 2: an odd signed-knapsack
 //! target and prime-power CRT encode the clauses. Only the actual normalized
-//! clauses need base-eight positions; widths zero through three use the same
-//! slack equation. Squaring uses twice the linear modulus, and extraction
+//! clauses need base-eight positions; deduplicated widths one through three
+//! use the same slack equation. Squaring uses twice the linear modulus, and extraction
 //! orients every sign by the distinguished odd coordinate.
 
 use std::collections::{BTreeMap, BTreeSet};
@@ -195,7 +195,7 @@ fn build_construction(
         coefficients[2 * j + 1] = -&half_weight;
         coefficients[2 * j + 2] = -BigInt::from(weight.clone());
         let width =
-            i64::try_from(clause.len()).expect("native K3 clauses have at most three literals");
+            i64::try_from(clause.len()).expect("deduplicated clauses have one to three literals");
         tau += (width - 5) * &half_weight;
         for &literal in clause {
             let variable =
diff --git a/src/rules/ksatisfiability_qubo.rs b/src/rules/ksatisfiability_qubo.rs
index f6d4d2337..c7ab13983 100644
--- a/src/rules/ksatisfiability_qubo.rs
+++ b/src/rules/ksatisfiability_qubo.rs
@@ -278,8 +278,8 @@ fn add_3sat_clause_penalty(
 }
 
 /// Expand clause penalties and retain the constant omitted by QUBO.
-/// K3 reserves one auxiliary per clause, including free auxiliaries for short
-/// clauses; K2 reserves none. The source constructor validates clause widths.
+/// K3 reserves one auxiliary per clause; K2 reserves none. The source
+/// constructor guarantees every clause has exactly K literals.
 fn build_qubo_matrix(
     num_vars: usize,
     clauses: &[crate::models::formula::CNFClause],
@@ -301,20 +301,15 @@ fn build_qubo_matrix(
             .map(|(variable, &literal)| (variable, literal < 0))
             .collect();
         let offset = match literals.as_slice() {
-            [] => 1,
-            &[(v, neg)] => {
-                add_coefficient(&mut matrix, v, v, if neg { 1 } else { -1 })?;
-                i64::from(!neg)
-            }
-            &[(_, n1), (_, n2)] => {
+            [(_, n1), (_, n2)] => {
                 add_2sat_clause_penalty(&mut matrix, &literals)?;
                 i64::from(!n1 && !n2)
             }
-            &[(_, n1), (_, n2), _] => {
+            [(_, n1), (_, n2), _] => {
                 add_3sat_clause_penalty(&mut matrix, &literals, num_vars + idx)?;
                 2 * i64::from(!n1 && !n2)
             }
-            _ => unreachable!("the source validates clause width at most three"),
+            _ => unreachable!("the source validates clause width two or three"),
         };
         constant = constant
             .checked_add(offset)
diff --git a/src/rules/ksatisfiability_registersufficiency.rs b/src/rules/ksatisfiability_registersufficiency.rs
index c4acc61c9..537d429dc 100644
--- a/src/rules/ksatisfiability_registersufficiency.rs
+++ b/src/rules/ksatisfiability_registersufficiency.rs
@@ -1,8 +1,7 @@
 //! Reduction from KSatisfiability (3-SAT) to RegisterSufficiency.
 //!
-//! This is Sethi's Reduction I / Theorem 3.11 (STOC 1973), with native
-//! empty-formula/empty-clause boundary targets, compact variables, and literal
-//! repetition for nonempty short clauses. The corrected extraction
+//! This is Sethi's Reduction I / Theorem 3.11 (STOC 1973), with an
+//! empty-formula boundary target and compact variables. The corrected extraction
 //! rule from issue #872:
 //! - the snapshot is taken immediately after `w[n]`
 //! - `x_k = true` iff `x_pos[k]` has been computed by that snapshot
@@ -337,15 +336,10 @@ impl ReduceTo<RegisterSufficiency> for KSatisfiability<K3> {
     type Result = Reduction3SATToRegisterSufficiency;
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        let empty_clause = self
-            .clauses()
-            .iter()
-            .any(|clause| clause.literals.is_empty());
-        if empty_clause || self.num_clauses() == 0 {
-            // Zero vertices need zero registers (YES); one output vertex
-            // cannot be computed with zero registers (NO).
+        if self.num_clauses() == 0 {
+            // Zero vertices need zero registers (YES).
             return Ok(Reduction3SATToRegisterSufficiency {
-                target: RegisterSufficiency::new(usize::from(empty_clause), Vec::new(), 0),
+                target: RegisterSufficiency::new(0, Vec::new(), 0),
                 layout: None,
                 source_num_vars: self.num_vars(),
                 source_variables: Vec::new(),
@@ -378,11 +372,6 @@ impl ReduceTo<RegisterSufficiency> for KSatisfiability<K3> {
                     let variable = i64::try_from(compact + 1).expect("compact SAT indices fit i64");
                     literals[position] = if literal > 0 { variable } else { -variable };
                 }
-                // Repeating a literal preserves a nonempty disjunction. Every
-                // slot has a real literal and the original first-true lock proof.
-                for position in clause.literals.len()..3 {
-                    literals[position] = literals[0];
-                }
                 literals
             })
             .collect();
diff --git a/src/rules/ksatisfiability_subsetsum.rs b/src/rules/ksatisfiability_subsetsum.rs
index 3efa0a862..78f420ef9 100644
--- a/src/rules/ksatisfiability_subsetsum.rs
+++ b/src/rules/ksatisfiability_subsetsum.rs
@@ -74,9 +74,13 @@ impl crate::rules::AggregateReductionResult for Reduction3SATToSubsetSum {}
 
 // Every integer has at most n+m decimal digits, and 10 < 2^4. The extra 1
 // also covers the empty formula's zero target (whose magnitude parameter is 1).
-#[reduction(transform = upper_bound {
-    num_elements = "2 * num_vars + 2 * num_clauses",
-    max_numeric_magnitude_bits = "4 * (num_vars + num_clauses) + 1",
+#[reduction(transform = {
+    exact {
+        num_elements = "2 * num_vars + 2 * num_clauses",
+    },
+    upper_bound {
+        max_numeric_magnitude_bits = "4 * (num_vars + num_clauses) + 1",
+    },
 })]
 impl ReduceTo<SubsetSum> for KSatisfiability<K3> {
     type Result = Reduction3SATToSubsetSum;
diff --git a/src/rules/maxcut_minimummatrixcover.rs b/src/rules/maxcut_minimummatrixcover.rs
index a1e8f50c7..65ab21868 100644
--- a/src/rules/maxcut_minimummatrixcover.rs
+++ b/src/rules/maxcut_minimummatrixcover.rs
@@ -1,21 +1,25 @@
 //! Reduction from MaxCut to MinimumMatrixCover.
 //!
-//! Given a MaxCut instance `(G, w)` with nonnegative integer edge weights,
-//! the target matrix `A` is the symmetric weighted adjacency matrix of `G`:
+//! For nonnegative edge weights, the target matrix `A` is the symmetric
+//! weighted adjacency matrix of `G`:
 //!     `a_{ij} = w({i, j})` if `{i, j} ∈ E`, otherwise `0` (diagonal is `0`).
 //!
 //! The key identity is
 //!     `Σ_{i,j} a_{ij} · f(i) · f(j) = 2 W − 4 · cut(S)`,
 //! where `S = { i : f(i) = +1 }` and `W = Σ_{e ∈ E} w(e)`. Minimizing the
 //! quadratic form is therefore equivalent to maximizing the cut, and the
-//! reduction is witness-preserving via the identity map between MaxCut's
+//! original vertices keep their bits between MaxCut's
 //! partition encoding (`config[i] = 1 ⇔ i ∈ S`) and MinimumMatrixCover's
 //! sign encoding (`config[i] = 1 ⇔ f(i) = +1 ⇔ i ∈ S`).
 //!
-//! **Precondition:** all edge weights must be nonnegative. The reduction
-//! panics on any negative weight, since `MinimumMatrixCover` requires a
-//! nonnegative integer matrix. Negative-weight `MaxCut` instances are out
-//! of scope and must use a different (preprocessing) reduction.
+//! `MinimumMatrixCover` requires a nonnegative matrix, so each negative edge
+//! `{u, v}` with weight `w < 0` becomes an auxiliary vertex `t` joined to `v`
+//! by weight `|w| + 1` and to `u` by weight `|w|`. Moving `t` to the side
+//! opposite `v` gains `|w| + 1` and loses at most `|w|`, so every maximum cut
+//! separates `t` from `v`. Then `t` is cut from `u` exactly when `u` and `v`
+//! share a side, and `|w| · [u, v same side] = w · [u, v cut] + |w|`: each
+//! gadget shifts the cut by the constant `2|w| + 1`. Maximum cuts, and so
+//! optimal sign assignments, correspond after dropping auxiliary vertices.
 //!
 //! Reference: Garey & Johnson, *Computers and Intractability* (1979),
 //! Appendix A1.2, MS13 ("Transformation from MAXIMUM CUT").
@@ -30,6 +34,7 @@ use crate::topology::{Graph, SimpleGraph};
 #[derive(Debug, Clone)]
 pub struct ReductionMaxCutToMMC {
     target: MinimumMatrixCover,
+    num_source_vertices: usize,
 }
 
 impl ReductionResult for ReductionMaxCutToMMC {
@@ -40,7 +45,7 @@ impl ReductionResult for ReductionMaxCutToMMC {
         &self.target
     }
 
-    /// Solution extraction is the identity.
+    /// Solution extraction keeps the source vertices' bits.
     ///
     /// Both encodings agree that bit `i = 1` means vertex `i` is in `S`:
     /// MaxCut treats `config[i] = 1` as one side of the partition, and
@@ -54,13 +59,14 @@ impl ReductionResult for ReductionMaxCutToMMC {
     ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
         crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
 
-        Ok(target_solution.to_vec())
+        Ok(target_solution[..self.num_source_vertices].to_vec())
     }
 }
 
 #[reduction(
-    transform = exact {
-        num_rows = "num_vertices",
+    transform = upper_bound {
+        // One auxiliary row per negative-weight edge.
+        num_rows = "num_vertices + num_edges",
     }
 )]
 impl ReduceTo<MinimumMatrixCover> for MaxCut<SimpleGraph, i64> {
@@ -68,24 +74,59 @@ impl ReduceTo<MinimumMatrixCover> for MaxCut<SimpleGraph, i64> {
 
     fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
         let n = self.graph().num_vertices();
-        let mut matrix: Vec<Vec<i64>> = vec![vec![0i64; n]; n];
+        let edges = self.edges();
+        let overflow = || {
+            crate::rules::ReductionError::integer_overflow::<Self, MinimumMatrixCover>(
+                "bounding the matrix-cover objective",
+            )
+        };
+        // All entries are nonnegative. Their sum is attained by equal signs and
+        // bounds the absolute value of every signed evaluation prefix. Checking
+        // this sum is therefore necessary and sufficient for i64 evaluation.
+        let mut matrix_sum = 0_i64;
+        for &(_, _, weight) in &edges {
+            let link_sum = if weight < 0 {
+                weight
+                    .checked_neg()
+                    .and_then(|magnitude| magnitude.checked_mul(2))
+                    .and_then(|sum| sum.checked_add(1))
+            } else {
+                Some(weight)
+            }
+            .ok_or_else(overflow)?;
+            matrix_sum = link_sum
+                .checked_mul(2)
+                .and_then(|sum| matrix_sum.checked_add(sum))
+                .ok_or_else(overflow)?;
+        }
+        let size = n + edges.iter().filter(|&&(_, _, w)| w < 0).count();
+        let mut matrix: Vec<Vec<i64>> = vec![vec![0i64; size]; size];
+        let mut link = |a: usize, b: usize, weight: i64| {
+            matrix[a][b] = weight;
+            matrix[b][a] = weight;
+        };
 
-        for (u, v, w) in self.edges() {
-            if w < 0 {
-                return Err(crate::rules::ReductionError::invalid_target::<
+        let mut auxiliary = n;
+        for (u, v, w) in edges {
+            if w >= 0 {
+                link(u, v, w);
+                continue;
+            }
+            // anchor = |w| + 1 = 1 - w; then |w| = anchor - 1 cannot overflow.
+            let Some(anchor) = 1_i64.checked_sub(w) else {
+                return Err(crate::rules::ReductionError::integer_overflow::<
                     MaxCut<SimpleGraph, i64>,
                     MinimumMatrixCover,
-                >(format!(
-                    "edge ({u}, {v}) has negative weight {w}"
-                )));
-            }
-            let w64 = w;
-            matrix[u][v] = w64;
-            matrix[v][u] = w64;
+                >("negating a negative edge weight"));
+            };
+            link(auxiliary, v, anchor);
+            link(auxiliary, u, anchor - 1);
+            auxiliary += 1;
         }
 
         Ok(ReductionMaxCutToMMC {
             target: MinimumMatrixCover::new(matrix),
+            num_source_vertices: n,
         })
     }
 }
diff --git a/src/rules/maximalis_ilp.rs b/src/rules/maximalis_ilp.rs
index 1f8ebb2fb..2e3bbb9b3 100644
--- a/src/rules/maximalis_ilp.rs
+++ b/src/rules/maximalis_ilp.rs
@@ -37,11 +37,11 @@ impl ReductionResult for ReductionMxISToILP {
 #[reduction(transform = {
     exact {
         num_vars = "num_vertices",
+        num_constraints = "num_edges + num_vertices",
+        num_nonzeros = "4 * num_edges + num_vertices",
     },
     upper_bound {
         max_constraint_magnitude_bits = "2 * num_edges + 2",
-        num_constraints = "num_edges + num_vertices",
-        num_nonzeros = "4 * num_edges + num_vertices",
     },
 })]
 impl ReduceTo<ILP<bool>> for MaximalIS<SimpleGraph, i64> {
diff --git a/src/rules/maximum2satisfiability_maxcut.rs b/src/rules/maximum2satisfiability_maxcut.rs
index e153b5d4f..f2340a3d4 100644
--- a/src/rules/maximum2satisfiability_maxcut.rs
+++ b/src/rules/maximum2satisfiability_maxcut.rs
@@ -62,9 +62,13 @@ fn literal_polarity(lit: i64) -> i64 {
 }
 
 #[reduction(
-    transform = upper_bound {
-        num_vertices = "num_vars + 1",
-        num_edges = "(num_vars + 1)^2",
+    transform = {
+        exact {
+            num_vertices = "num_vars + 1",
+        },
+        upper_bound {
+            num_edges = "(num_vars + 1)^2",
+        },
     }
 )]
 impl ReduceTo<MaxCut<SimpleGraph, i64>> for Maximum2Satisfiability {
diff --git a/src/rules/maximummatching_ilp.rs b/src/rules/maximummatching_ilp.rs
index 42f1a3799..ab0f0a9f8 100644
--- a/src/rules/maximummatching_ilp.rs
+++ b/src/rules/maximummatching_ilp.rs
@@ -48,11 +48,11 @@ impl ReductionResult for ReductionMatchingToILP {
 #[reduction(transform = {
     exact {
         num_vars = "num_edges",
+        num_nonzeros = "2 * num_edges",
     },
     upper_bound {
         max_constraint_magnitude_bits = "2",
         num_constraints = "num_vertices",
-        num_nonzeros = "2 * num_edges",
     },
 })]
 impl ReduceTo<ILP<bool>> for MaximumMatching<SimpleGraph, i64> {
diff --git a/src/rules/minimumdominatingset_ilp.rs b/src/rules/minimumdominatingset_ilp.rs
index 7f3007d82..db2ea9980 100644
--- a/src/rules/minimumdominatingset_ilp.rs
+++ b/src/rules/minimumdominatingset_ilp.rs
@@ -52,10 +52,10 @@ impl ReductionResult for ReductionDSToILP {
     exact {
         num_vars = "num_vertices",
         num_constraints = "num_vertices",
+        num_nonzeros = "2 * num_edges + num_vertices",
     },
     upper_bound {
         max_constraint_magnitude_bits = "2 * num_edges + 2",
-        num_nonzeros = "2 * num_edges + num_vertices",
     },
 })]
 impl ReduceTo<ILP<bool>> for MinimumDominatingSet<SimpleGraph, i64> {
diff --git a/src/rules/minimumsummulticenter_ilp.rs b/src/rules/minimumsummulticenter_ilp.rs
index a714ec003..2b131677d 100644
--- a/src/rules/minimumsummulticenter_ilp.rs
+++ b/src/rules/minimumsummulticenter_ilp.rs
@@ -117,11 +117,15 @@ fn weighted_distances_msmc(
     dist
 }
 
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "num_vertices + 1",
-    num_vars = "num_vertices + num_vertices^2",
-    num_constraints = "num_vertices^2 + 2 * num_vertices + 1",
-    num_nonzeros = "3 * num_vertices^2 + num_vertices",
+#[reduction(transform = {
+    exact {
+        num_vars = "num_vertices + num_vertices^2",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "num_vertices + 1",
+        num_constraints = "num_vertices^2 + 2 * num_vertices + 1",
+        num_nonzeros = "3 * num_vertices^2 + num_vertices",
+    },
 })]
 impl ReduceTo<ILP<bool>> for MinimumSumMulticenter<SimpleGraph, i64> {
     type Result = ReductionMSMCToILP;
diff --git a/src/rules/minimumvertexcover_ensemblecomputation.rs b/src/rules/minimumvertexcover_ensemblecomputation.rs
index 710badf1f..a625c5c08 100644
--- a/src/rules/minimumvertexcover_ensemblecomputation.rs
+++ b/src/rules/minimumvertexcover_ensemblecomputation.rs
@@ -76,10 +76,14 @@ impl ReductionResult for ReductionVCToEC {
 }
 
 #[reduction(
-    transform = upper_bound {
-        universe_size = "num_vertices + 1",
-        num_subsets = "num_edges",
-        budget = "num_vertices + num_edges + 1",
+    transform = {
+        exact {
+            universe_size = "num_vertices + 1",
+            num_subsets = "num_edges",
+        },
+        upper_bound {
+            budget = "num_vertices + num_edges + 1",
+        },
     }
 )]
 impl ReduceTo<EnsembleComputation> for MinimumVertexCover<SimpleGraph, One> {
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index 5815a32ed..e9d97f464 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -68,7 +68,6 @@ pub(crate) mod kcoloring_twodimensionalconsecutivesets;
 mod knapsack_qubo;
 pub(crate) mod ksatisfiability_acyclicpartition;
 pub(crate) mod ksatisfiability_bicliquecover;
-mod ksatisfiability_casts;
 pub(crate) mod ksatisfiability_cyclicordering;
 pub(crate) mod ksatisfiability_decisionminimumvertexcover;
 pub(crate) mod ksatisfiability_directedtwocommodityintegralflow;
diff --git a/src/rules/numericalmatchingwithtargetsums_ilp.rs b/src/rules/numericalmatchingwithtargetsums_ilp.rs
index 83a8b9df8..45cff4eb0 100644
--- a/src/rules/numericalmatchingwithtargetsums_ilp.rs
+++ b/src/rules/numericalmatchingwithtargetsums_ilp.rs
@@ -70,11 +70,15 @@ impl ReductionResult for ReductionNMTSToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionNMTSToILP {}
 
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "1",
-    num_vars = "num_pairs * num_pairs * num_pairs",
-    num_constraints = "3 * num_pairs",
-    num_nonzeros = "3 * num_pairs * num_pairs * num_pairs",
+#[reduction(transform = {
+    exact {
+        num_constraints = "3 * num_pairs",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "1",
+        num_vars = "num_pairs * num_pairs * num_pairs",
+        num_nonzeros = "3 * num_pairs * num_pairs * num_pairs",
+    },
 })]
 impl ReduceTo<ILP<bool>> for NumericalMatchingWithTargetSums {
     type Result = ReductionNMTSToILP;
diff --git a/src/rules/partitionintocliques_minimumcoveringbycliques.rs b/src/rules/partitionintocliques_minimumcoveringbycliques.rs
index 1c4639752..d090e7173 100644
--- a/src/rules/partitionintocliques_minimumcoveringbycliques.rs
+++ b/src/rules/partitionintocliques_minimumcoveringbycliques.rs
@@ -208,7 +208,7 @@ impl crate::rules::AggregateReductionResult
 }
 
 #[reduction(
-    transform = upper_bound {
+    transform = exact {
         num_vertices = "2 * num_vertices + 4 * num_edges + 4",
         num_edges = "(num_vertices + 2 * num_edges)^2 + 4 * num_vertices + 14 * num_edges + 2",
     }
diff --git a/src/rules/partitionintopathsoflength2_ilp.rs b/src/rules/partitionintopathsoflength2_ilp.rs
index 8477633c7..6e6d7b065 100644
--- a/src/rules/partitionintopathsoflength2_ilp.rs
+++ b/src/rules/partitionintopathsoflength2_ilp.rs
@@ -67,13 +67,17 @@ impl ReductionResult for ReductionPIPL2ToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionPIPL2ToILP {}
 
-// With q=floor(n/3) and e distinct non-loop edges: q(n+e) variables,
-// n+2q+3eq rows, and 2nq+8eq terms. Deduplication gives e<=num_edges.
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "2",
-    num_vars = "num_vertices * (num_vertices + num_edges) / 3",
-    num_constraints = "5 * num_vertices / 3 + num_edges * num_vertices",
-    num_nonzeros = "(2 * num_vertices^2 + 8 * num_edges * num_vertices) / 3",
+// Construction requires 3 | n and SimpleGraph has no loops or repeated edges,
+// so q = n/3 and e = num_edges: q(n+e) variables, n+2q+3eq rows, 2nq+8eq terms.
+#[reduction(transform = {
+    exact {
+        num_vars = "num_vertices * (num_vertices + num_edges) / 3",
+        num_constraints = "5 * num_vertices / 3 + num_edges * num_vertices",
+        num_nonzeros = "(2 * num_vertices^2 + 8 * num_edges * num_vertices) / 3",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "2",
+    },
 })]
 impl ReduceTo<ILP<bool>> for PartitionIntoPathsOfLength2<SimpleGraph> {
     type Result = ReductionPIPL2ToILP;
diff --git a/src/rules/partitionintoperfectmatchings_ilp.rs b/src/rules/partitionintoperfectmatchings_ilp.rs
index 95add09a6..80e09cb58 100644
--- a/src/rules/partitionintoperfectmatchings_ilp.rs
+++ b/src/rules/partitionintoperfectmatchings_ilp.rs
@@ -27,11 +27,15 @@ impl ReductionResult for ReductionPartitionIntoPerfectMatchingsToILP {
 }
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionPartitionIntoPerfectMatchingsToILP {}
-#[crate::reduction(transform = upper_bound {
-    num_vars = "num_vertices + 2 * num_edges",
-    num_constraints = "num_vertices + 4 * num_edges",
-    num_nonzeros = "16 * num_edges",
-    max_constraint_magnitude_bits = "num_matchings",
+#[crate::reduction(transform = {
+    exact {
+        num_vars = "num_vertices + 2 * num_edges",
+        num_constraints = "num_vertices + 4 * num_edges",
+    },
+    upper_bound {
+        num_nonzeros = "16 * num_edges",
+        max_constraint_magnitude_bits = "num_matchings",
+    },
 })]
 impl ReduceTo<ILP<i64, i64, Bounded>> for PartitionIntoPerfectMatchings<SimpleGraph> {
     type Result = ReductionPartitionIntoPerfectMatchingsToILP;
diff --git a/src/rules/sat_ksat.rs b/src/rules/sat_ksat.rs
index fd5607f92..966f7ae1a 100644
--- a/src/rules/sat_ksat.rs
+++ b/src/rules/sat_ksat.rs
@@ -10,7 +10,7 @@ use crate::models::formula::{CNFClause, KSatisfiability, Satisfiability};
 use crate::reduction;
 use crate::rules::sat_helpers::SatVariableAllocator;
 use crate::rules::traits::{ReduceTo, ReductionResult};
-use crate::variant::{KValue, K2, K3, KN};
+use crate::variant::{KValue, K2, K3};
 
 /// Result of reducing general SAT to K-SAT.
 ///
@@ -50,8 +50,6 @@ impl<K: KValue> ReductionResult for ReductionSATToKSAT<K> {
     }
 }
 
-crate::register_aggregate_reduction!(ReductionSATToKSAT<K3>);
-
 #[crate::aggregate_reduction(identity)]
 impl<K: KValue> crate::rules::AggregateReductionResult for ReductionSATToKSAT<K> {}
 
@@ -128,6 +126,8 @@ fn add_clause_to_ksat(
 /// because the `#[reduction]` proc macro requires concrete types.
 macro_rules! impl_sat_to_ksat {
     ($ktype:ty, $k:expr) => {
+        crate::register_aggregate_reduction!(ReductionSATToKSAT<$ktype>);
+
         #[rustfmt::skip]
         #[reduction(transform = upper_bound {
             num_clauses = "8 * num_clauses + num_literals",
@@ -206,8 +206,6 @@ impl<K: KValue> ReductionResult for ReductionKSATToSAT<K> {
     }
 }
 
-crate::register_aggregate_reduction!(ReductionKSATToSAT<KN>);
-
 #[crate::aggregate_reduction(identity)]
 impl<K: KValue> crate::rules::AggregateReductionResult for ReductionKSATToSAT<K> {}
 
@@ -226,6 +224,8 @@ fn reduce_ksat_to_sat<K: KValue>(ksat: &KSatisfiability<K>) -> ReductionKSATToSA
 /// The `#[reduction]` macro requires concrete types.
 macro_rules! impl_ksat_to_sat {
     ($ktype:ty) => {
+        crate::register_aggregate_reduction!(ReductionKSATToSAT<$ktype>);
+
 #[rustfmt::skip]
         #[reduction(
     transform = exact {
@@ -243,24 +243,8 @@ macro_rules! impl_ksat_to_sat {
     };
 }
 
-// Register KN for the reduction graph (covers all K values as the generic entry)
-impl_ksat_to_sat!(KN);
-
-// K3 and K2 keep their ReduceTo<Satisfiability> impls for typed use,
-// but are NOT registered as separate primitive graph edges (KN covers them).
-impl ReduceTo<Satisfiability> for KSatisfiability<K3> {
-    type Result = ReductionKSATToSAT<K3>;
-    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        Ok(reduce_ksat_to_sat(self))
-    }
-}
-
-impl ReduceTo<Satisfiability> for KSatisfiability<K2> {
-    type Result = ReductionKSATToSAT<K2>;
-    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
-        Ok(reduce_ksat_to_sat(self))
-    }
-}
+impl_ksat_to_sat!(K2);
+impl_ksat_to_sat!(K3);
 
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
@@ -297,7 +281,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
         crate::example_db::specs::RuleExampleSpec {
             id: "ksatisfiability_to_satisfiability",
             build: || {
-                let source = KSatisfiability::<KN>::new(
+                let source = KSatisfiability::<K3>::new(
                     4,
                     vec![
                         CNFClause::new(vec![1, -2, 3]),
@@ -314,6 +298,26 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
                 )
             },
         },
+        crate::example_db::specs::RuleExampleSpec {
+            id: "ksatisfiability_k2_to_satisfiability",
+            build: || {
+                let source = KSatisfiability::<K2>::new(
+                    3,
+                    vec![
+                        CNFClause::new(vec![1, -2]),
+                        CNFClause::new(vec![2, 3]),
+                        CNFClause::new(vec![-1, -3]),
+                    ],
+                );
+                crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
+                    source,
+                    SolutionPair {
+                        source_config: serde_json::json!(vec![true, true, false]),
+                        target_config: serde_json::json!(vec![true, true, false]),
+                    },
+                )
+            },
+        },
     ]
 }
 
diff --git a/src/rules/shortestcommonsupersequence_ilp.rs b/src/rules/shortestcommonsupersequence_ilp.rs
index 636d06962..9dbe64439 100644
--- a/src/rules/shortestcommonsupersequence_ilp.rs
+++ b/src/rules/shortestcommonsupersequence_ilp.rs
@@ -49,11 +49,15 @@ impl ReductionResult for ReductionSCSToILP {
 // contribute b(a+1)+3Lb terms, order rows <=2Lb, padding <=2b.
 // Zero positional coefficients disappear. Coefficients <=max(1,b-1)
 // require at most ceil(b/2+1) bits, including b=0.
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "max_length / 2 + 1",
-    num_vars = "max_length * (alphabet_size + 1) + total_length * max_length",
-    num_constraints = "max_length + total_length + total_length * max_length + total_length + max_length",
-    num_nonzeros = "max_length * (alphabet_size + 3) + 5 * total_length * max_length",
+#[reduction(transform = {
+    exact {
+        num_vars = "max_length * (alphabet_size + 1) + total_length * max_length",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "max_length / 2 + 1",
+        num_constraints = "max_length + total_length + total_length * max_length + total_length + max_length",
+        num_nonzeros = "max_length * (alphabet_size + 3) + 5 * total_length * max_length",
+    },
 })]
 impl ReduceTo<ILP<bool>> for ShortestCommonSupersequence {
     type Result = ReductionSCSToILP;
diff --git a/src/rules/sparsematrixcompression_ilp.rs b/src/rules/sparsematrixcompression_ilp.rs
index 6156f5e2c..fcdc44d46 100644
--- a/src/rules/sparsematrixcompression_ilp.rs
+++ b/src/rules/sparsematrixcompression_ilp.rs
@@ -47,11 +47,15 @@ impl crate::rules::AggregateReductionResult for ReductionSMCToILP {}
 
 // Assignments contribute r*k terms. Each unordered row pair and pair
 // of columns emits at most k two-term collision rows; empty columns add none.
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "1",
-    num_vars = "num_rows * bound_k",
-    num_constraints = "num_rows + num_rows * (num_rows - 1) * num_cols^2 * bound_k / 2",
-    num_nonzeros = "num_rows * bound_k + num_rows * (num_rows - 1) * num_cols^2 * bound_k",
+#[reduction(transform = {
+    exact {
+        num_vars = "num_rows * bound_k",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "1",
+        num_constraints = "num_rows + num_rows * (num_rows - 1) * num_cols^2 * bound_k / 2",
+        num_nonzeros = "num_rows * bound_k + num_rows * (num_rows - 1) * num_cols^2 * bound_k",
+    },
 })]
 impl ReduceTo<ILP<bool>> for SparseMatrixCompression {
     type Result = ReductionSMCToILP;
diff --git a/src/rules/strongconnectivityaugmentation_ilp.rs b/src/rules/strongconnectivityaugmentation_ilp.rs
index 233a99613..af2ecb5d8 100644
--- a/src/rules/strongconnectivityaugmentation_ilp.rs
+++ b/src/rules/strongconnectivityaugmentation_ilp.rs
@@ -50,9 +50,9 @@ impl crate::rules::AggregateReductionResult for ReductionSCAToILP {}
 #[reduction(transform = {
     exact {
         max_constraint_magnitude_bits = "max_numeric_magnitude_bits",
+        num_vars = "num_potential_arcs + 2 * num_vertices * (num_arcs + num_potential_arcs)",
     },
     upper_bound {
-        num_vars = "num_potential_arcs + 2 * num_vertices * (num_arcs + num_potential_arcs)",
         num_constraints = "1 + num_potential_arcs + 2 * num_arcs + 2 * num_vertices * num_potential_arcs + 2 * num_vertices * num_vertices",
         num_nonzeros = "2 * num_potential_arcs + num_vertices * (4 * num_arcs + 8 * num_potential_arcs)",
     },
diff --git a/src/rules/subgraphisomorphism_ilp.rs b/src/rules/subgraphisomorphism_ilp.rs
index dccbb54c4..e7252e364 100644
--- a/src/rules/subgraphisomorphism_ilp.rs
+++ b/src/rules/subgraphisomorphism_ilp.rs
@@ -57,11 +57,15 @@ impl ReductionResult for ReductionSubIsoToILP {
 #[crate::aggregate_reduction(ilp_feasibility)]
 impl crate::rules::AggregateReductionResult for ReductionSubIsoToILP {}
 
-#[reduction(transform = upper_bound {
-    max_constraint_magnitude_bits = "2",
-    num_vars = "num_pattern_vertices * num_host_vertices",
-    num_constraints = "num_pattern_vertices + num_host_vertices + num_pattern_edges * num_host_vertices^2",
-    num_nonzeros = "2 * num_pattern_vertices * num_host_vertices + 2 * num_pattern_edges * num_host_vertices^2",
+#[reduction(transform = {
+    exact {
+        num_vars = "num_pattern_vertices * num_host_vertices",
+    },
+    upper_bound {
+        max_constraint_magnitude_bits = "2",
+        num_constraints = "num_pattern_vertices + num_host_vertices + num_pattern_edges * num_host_vertices^2",
+        num_nonzeros = "2 * num_pattern_vertices * num_host_vertices + 2 * num_pattern_edges * num_host_vertices^2",
+    },
 })]
 impl ReduceTo<ILP<bool>> for SubgraphIsomorphism {
     type Result = ReductionSubIsoToILP;
diff --git a/src/rules/undirectedflowlowerbounds_ilp.rs b/src/rules/undirectedflowlowerbounds_ilp.rs
index 19ad6e55a..69bcede2a 100644
--- a/src/rules/undirectedflowlowerbounds_ilp.rs
+++ b/src/rules/undirectedflowlowerbounds_ilp.rs
@@ -80,11 +80,15 @@ impl ReductionResult for ReductionUFLBToILP {
 impl crate::rules::AggregateReductionResult for ReductionUFLBToILP {}
 
 #[reduction(
-    transform = upper_bound {
-        max_constraint_magnitude_bits = "max_capacity_bits + num_edges + 1",
-        num_vars = "3 * num_edges",
-        num_constraints = "5 * num_edges + num_vertices + 1",
-        num_nonzeros = "13 * num_edges",
+    transform = {
+        exact {
+            num_vars = "3 * num_edges",
+        },
+        upper_bound {
+            max_constraint_magnitude_bits = "max_capacity_bits + num_edges + 1",
+            num_constraints = "5 * num_edges + num_vertices + 1",
+            num_nonzeros = "13 * num_edges",
+        },
     },
 )]
 impl ReduceTo<ILP<i64, i64, Bounded>> for UndirectedFlowLowerBounds {
diff --git a/src/solvers/pipelines.rs b/src/solvers/pipelines.rs
index 4260a470d..b9615dead 100644
--- a/src/solvers/pipelines.rs
+++ b/src/solvers/pipelines.rs
@@ -278,7 +278,7 @@ register_ilp_pipeline! {
 }
 
 register_ilp_pipeline! {
-    ("KSatisfiability", [("k", "KN")]),
+    ("KSatisfiability", [("k", "K3")]),
     ("Satisfiability", []),
     ("NAESatisfiability", []),
     ("ILP", [("variable", "bool"), ("coefficient", "i64"), ("bounds", "general")]),
diff --git a/src/unit_tests/ilp_overhead.rs b/src/unit_tests/ilp_overhead.rs
index 5b33193a1..c1c17fcfe 100644
--- a/src/unit_tests/ilp_overhead.rs
+++ b/src/unit_tests/ilp_overhead.rs
@@ -205,27 +205,24 @@ fn nae_support_ignores_repeated_literals_and_bounds_cancellation() {
 fn timetable_counts_core_edges_and_their_available_colors() {
     use crate::models::formula::{CNFClause, KSatisfiability};
     use crate::variant::K3;
-    let source = KSatisfiability::<K3>::new_allow_less(
+    let source = KSatisfiability::<K3>::new(
         1,
-        vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
+        vec![
+            CNFClause::new(vec![1, 1, 1]),
+            CNFClause::new(vec![-1, -1, -1]),
+        ],
     );
-    // Six two-list variable edges each supply three edges with two colors;
-    // the two singleton clause edges each supply one available assignment.
     check_counts::<_, TimetableDesign>(
         &source,
         &[
-            ("num_nonzero_requirements", 20, 48),
-            ("num_available_assignments", 38, 96),
-            ("period_count_bits", 3, 5),
-            ("num_craftsmen", 10, 23),
-            ("num_tasks", 10, 24),
+            ("num_nonzero_requirements", 128, 132),
+            ("num_available_assignments", 258, 264),
+            ("period_count_bits", 5, 9),
+            ("num_craftsmen", 61, 63),
+            ("num_tasks", 62, 64),
         ],
     );
-    check_contract::<_, TimetableDesign>(&KSatisfiability::<K3>::new_allow_less(0, vec![]));
-    check_contract::<_, TimetableDesign>(&KSatisfiability::<K3>::new_allow_less(
-        0,
-        vec![CNFClause::new(vec![])],
-    ));
+    check_contract::<_, TimetableDesign>(&KSatisfiability::<K3>::new(0, vec![]));
 }
 
 #[test]
@@ -396,9 +393,12 @@ fn ensemble_terms_include_ordering_and_target_matches() {
 fn changed_predictions_bound_real_intermediate_targets() {
     use crate::models::formula::{CNFClause, KSatisfiability, NAESatisfiability, Satisfiability};
     use crate::variant::K3;
-    let source = KSatisfiability::<K3>::new_allow_less(
+    let source = KSatisfiability::<K3>::new(
         1,
-        vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
+        vec![
+            CNFClause::new(vec![1, 1, 1]),
+            CNFClause::new(vec![-1, -1, -1]),
+        ],
     );
     for intermediate in [
         step::<TimetableDesign>(),
@@ -583,20 +583,14 @@ fn sentinel_literal_pairs_count_each_clause_once() {
 fn unit_schedule_bits_and_precedences_count_layers() {
     use crate::models::formula::{CNFClause, KSatisfiability};
     use crate::variant::K3;
-    // Capacities [1,3,3,6], seven processors, filler sizes [6,4,4,1].
-    // 4 variable links + 21 literal links + 24+16+4 filler links.
     check_counts::<_, PreemptiveScheduling>(
-        &KSatisfiability::<K3>::new_allow_less(1, vec![CNFClause::new(vec![1])]),
+        &KSatisfiability::<K3>::new(1, vec![CNFClause::new(vec![1, 1, 1])]),
         &[
             ("num_precedences", 69, 388),
             ("max_schedule_magnitude_bits", 5, 8),
         ],
     );
-    for clauses in [vec![], vec![CNFClause::new(vec![])]] {
-        check_contract::<_, PreemptiveScheduling>(&KSatisfiability::<K3>::new_allow_less(
-            0, clauses,
-        ));
-    }
+    check_contract::<_, PreemptiveScheduling>(&KSatisfiability::<K3>::new(0, vec![]));
 }
 
 #[test]
diff --git a/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs b/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs
index a0a0bf5d1..39874eba4 100644
--- a/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs
+++ b/src/unit_tests/models/algebraic/consecutive_ones_submatrix.rs
@@ -241,3 +241,12 @@ fn json_rejects_invalid_instance() {
     )
     .is_err());
 }
+
+#[test]
+fn json_rejects_negative_bound() {
+    // The bound counts columns, so its type rejects negative values.
+    assert!(serde_json::from_value::<ConsecutiveOnesSubmatrix>(
+        serde_json::json!({"matrix":[[true]],"bound":-1})
+    )
+    .is_err());
+}
diff --git a/src/unit_tests/models/formula/ksat.rs b/src/unit_tests/models/formula/ksat.rs
index 4ec78e2a4..72cdaee92 100644
--- a/src/unit_tests/models/formula/ksat.rs
+++ b/src/unit_tests/models/formula/ksat.rs
@@ -1,4 +1,5 @@
 use super::*;
+use crate::registry::ConstructionError;
 use crate::solvers::BruteForce;
 use crate::solvers::BruteForceProblem as _;
 use crate::traits::Problem;
@@ -70,16 +71,24 @@ fn test_3sat_brute_force() {
 }
 
 #[test]
-fn test_ksat_allow_less() {
-    // This should work - clause has 2 literals which is <= 3
-    let problem = KSatisfiability::<K3>::new_allow_less(2, vec![CNFClause::new(vec![1, 2])]);
-    assert_eq!(problem.num_clauses(), 1);
+fn test_ksat_rejects_clause_widths_other_than_k() {
+    for literals in [vec![], vec![1], vec![1, 2], vec![1, 2, 3, 4]] {
+        let width = literals.len();
+        let error = KSatisfiability::<K3>::try_new(4, vec![CNFClause::new(literals)]).unwrap_err();
+        assert_eq!(
+            error,
+            ConstructionError::Conversion(format!("Clause 0 has {width} literals, expected 3"))
+        );
+    }
 }
 
 #[test]
-#[should_panic(expected = "Clause 0 has 4 literals, expected at most 3")]
-fn test_ksat_allow_less_too_many() {
-    let _ = KSatisfiability::<K3>::new_allow_less(4, vec![CNFClause::new(vec![1, 2, 3, 4])]);
+fn test_ksat_rejects_unbounded_clause_width() {
+    let error = KSatisfiability::<KN>::try_new(1, vec![CNFClause::new(vec![1])]).unwrap_err();
+    assert_eq!(
+        error,
+        ConstructionError::Conversion("KSatisfiability requires a fixed clause width K".into())
+    );
 }
 
 #[test]
@@ -181,43 +190,6 @@ fn test_jl_parity_evaluation() {
     }
 }
 
-#[test]
-fn test_kn_creation() {
-    // KN accepts clauses of any length without validation
-    let problem = KSatisfiability::<KN>::new(
-        3,
-        vec![
-            CNFClause::new(vec![1, 2, 3]), // 3 literals
-            CNFClause::new(vec![-1, -2]),  // 2 literals
-            CNFClause::new(vec![1]),       // 1 literal
-        ],
-    );
-    assert_eq!(problem.num_vars(), 3);
-    assert_eq!(problem.num_clauses(), 3);
-    assert!(problem.evaluate(&vec![true, false, false]).unwrap()); // x1=T, x2=F, x3=F
-}
-
-#[test]
-fn test_kn_from_k3_clauses() {
-    // KN can be constructed from clauses originally built for K3
-    let k3 = KSatisfiability::<K3>::new(
-        3,
-        vec![
-            CNFClause::new(vec![1, 2, -3]),
-            CNFClause::new(vec![-1, -2, -3]),
-        ],
-    );
-    let kn = KSatisfiability::<KN>::new(k3.num_vars(), k3.clauses().to_vec());
-    // Both should agree on evaluations
-    for config in &[
-        vec![true, false, false],
-        vec![false, true, false],
-        vec![true, true, true],
-    ] {
-        assert_eq!(k3.evaluate(config).unwrap(), kn.evaluate(config).unwrap());
-    }
-}
-
 #[test]
 fn test_parameter_getters() {
     let problem = KSatisfiability::<K3>::new(
diff --git a/src/unit_tests/reduction_graph.rs b/src/unit_tests/reduction_graph.rs
index caa9d2744..2dcab2e53 100644
--- a/src/unit_tests/reduction_graph.rs
+++ b/src/unit_tests/reduction_graph.rs
@@ -810,8 +810,8 @@ fn default_variant_for_ksat_uses_declared_default() {
     let variant = default.unwrap();
     assert_eq!(
         variant.get("k").map(|s| s.as_str()),
-        Some("KN"),
-        "default KSatisfiability variant should use KN"
+        Some("K3"),
+        "default KSatisfiability variant should use K3"
     );
 }
 
diff --git a/src/unit_tests/rules/aggregate_contracts.rs b/src/unit_tests/rules/aggregate_contracts.rs
index af36839a9..c5aab992d 100644
--- a/src/unit_tests/rules/aggregate_contracts.rs
+++ b/src/unit_tests/rules/aggregate_contracts.rs
@@ -225,18 +225,15 @@ fn matching_decoding_threshold_handles_empty_and_unsatisfiable_instances() {
 }
 
 #[test]
-fn sat_cover_threshold_supports_short_and_empty_clauses() {
+fn sat_cover_threshold_supports_repeated_literals() {
     for clauses in [
         vec![],
-        vec![vec![]],
-        vec![vec![1]],
-        vec![vec![1], vec![-1]],
+        vec![vec![1, 1, 1]],
+        vec![vec![1, 1, 1], vec![-1, -1, -1]],
         vec![vec![1, -1, 1]],
     ] {
-        let source = KSatisfiability::<K3>::new_allow_less(
-            1,
-            clauses.into_iter().map(CNFClause::new).collect(),
-        );
+        let source =
+            KSatisfiability::<K3>::new(1, clauses.into_iter().map(CNFClause::new).collect());
         check_decision::<
             _,
             crate::models::decision::Decision<MinimumVertexCover<SimpleGraph, crate::types::One>>,
@@ -302,11 +299,11 @@ fn sat_empty_conjunction_and_empty_clause_preserve_opposite_answers() {
     use crate::models::graph::KColoring;
     use crate::models::misc::TimetableDesign;
     for clauses in [vec![], vec![CNFClause::new(vec![])]] {
-        let source = Satisfiability::new(0, clauses.clone());
+        let source = Satisfiability::new(0, clauses);
         check_decision::<_, KSatisfiability<K3>>(&source);
         check_decision::<_, KColoring<K3, SimpleGraph>>(&source);
-        check_decision::<_, TimetableDesign>(&KSatisfiability::<K3>::new_allow_less(0, clauses));
     }
+    check_decision::<_, TimetableDesign>(&KSatisfiability::<K3>::new(0, vec![]));
 }
 
 #[test]
diff --git a/src/unit_tests/rules/graph.rs b/src/unit_tests/rules/graph.rs
index c2cb4a0d3..d30d52b95 100644
--- a/src/unit_tests/rules/graph.rs
+++ b/src/unit_tests/rules/graph.rs
@@ -1892,7 +1892,7 @@ fn test_reduction_chain_with_variant_reductions() {
         )
         .into_iter()
         .find(|path| {
-            path.len() == 5
+            path.len() == 4
                 && path.type_names()
                     == [
                         "KSatisfiability",
diff --git a/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs b/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs
index 7b68f443c..b6bb1ce14 100644
--- a/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs
+++ b/src/unit_tests/rules/ksatisfiability_acyclicpartition.rs
@@ -86,7 +86,7 @@ fn test_acyclicpartition_extraction_rejects_invalid_targets() {
 }
 
 #[test]
-fn test_acyclicpartition_native_empty_and_short_clauses() {
+fn test_acyclicpartition_empty_and_unsatisfiable_formulas() {
     for n in [0, 3] {
         let source = KSatisfiability::<K3>::new(n, vec![]);
         let reduction = ReduceTo::<AcyclicPartition<i64>>::reduce_to(&source).unwrap();
@@ -103,19 +103,20 @@ fn test_acyclicpartition_native_empty_and_short_clauses() {
             );
         }
     }
-    for clauses in [vec![vec![]], vec![vec![1], vec![-1]]] {
-        let source = KSatisfiability::<K3>::new_allow_less(
-            1,
-            clauses.into_iter().map(CNFClause::new).collect(),
-        );
-        let reduction = ReduceTo::<AcyclicPartition<i64>>::reduce_to(&source).unwrap();
-        assert!(BruteForce::new().solve(&source).unwrap().is_none());
-        let items = reduction.target_problem().num_vertices() - 2;
-        for mask in 0..(1usize << items) {
-            let mut labels: Vec<usize> = (0..items).map(|i| (mask >> i) & 1).collect();
-            labels.extend([0, 1]);
-            assert!(!reduction.target_problem().evaluate(&labels).unwrap().0);
-        }
+    let source = KSatisfiability::<K3>::new(
+        1,
+        vec![
+            CNFClause::new(vec![1, 1, 1]),
+            CNFClause::new(vec![-1, -1, -1]),
+        ],
+    );
+    let reduction = ReduceTo::<AcyclicPartition<i64>>::reduce_to(&source).unwrap();
+    assert!(BruteForce::new().solve(&source).unwrap().is_none());
+    let items = reduction.target_problem().num_vertices() - 2;
+    for mask in 0..(1usize << items) {
+        let mut labels: Vec<usize> = (0..items).map(|i| (mask >> i) & 1).collect();
+        labels.extend([0, 1]);
+        assert!(!reduction.target_problem().evaluate(&labels).unwrap().0);
     }
 }
 
diff --git a/src/unit_tests/rules/ksatisfiability_bicliquecover.rs b/src/unit_tests/rules/ksatisfiability_bicliquecover.rs
index 9c6b4b2c9..901eb6fee 100644
--- a/src/unit_tests/rules/ksatisfiability_bicliquecover.rs
+++ b/src/unit_tests/rules/ksatisfiability_bicliquecover.rs
@@ -207,7 +207,7 @@ fn test_ksatisfiability_to_bicliquecover_construct_two_vars_no_panic() {
 fn test_ksatisfiability_to_bicliquecover_sparse_variable_inverse() {
     // The only used variable has a high source index. Its normalized gadget
     // equals the canonical one-variable gadget; unused variables map to false.
-    let source = KSatisfiability::<K3>::new_allow_less(7, vec![CNFClause::new(vec![7])]);
+    let source = KSatisfiability::<K3>::new(7, vec![CNFClause::new(vec![7, 7, 7])]);
     let reduction = ReduceTo::<BicliqueCover>::reduce_to(&source).unwrap();
     assert_eq!(reduction.source_variables, vec![6]);
     assert_eq!(reduction.normalized_n, 2);
@@ -237,30 +237,25 @@ fn test_ksatisfiability_to_bicliquecover_sparse_variable_inverse() {
 }
 
 #[test]
-fn test_ksatisfiability_to_bicliquecover_empty_conjunction_and_clause() {
+fn test_ksatisfiability_to_bicliquecover_empty_conjunction() {
     for n in [0, 3] {
         let yes = KSatisfiability::<K3>::new(n, vec![]);
         let reduction = ReduceTo::<BicliqueCover>::reduce_to(&yes).unwrap();
         assert_eq!(reduction.target_problem().num_vertices(), 0);
         assert_eq!(reduction.extract_solution(&vec![]).unwrap(), vec![false; n]);
         assert!(yes.evaluate(&vec![false; n]).unwrap().0);
-        let no = KSatisfiability::<K3>::new_allow_less(n, vec![CNFClause::new(vec![])]);
-        let reduction = ReduceTo::<BicliqueCover>::reduce_to(&no).unwrap();
-        assert!(reduction
-            .target_problem()
-            .evaluate(&vec![])
-            .unwrap()
-            .0
-            .is_none());
-        assert!(reduction.extract_solution(&vec![]).is_err());
-        assert!(!no.evaluate(&vec![false; n]).unwrap().0);
     }
 }
 
 #[test]
-fn test_ksatisfiability_to_bicliquecover_normalization_preserves_short_clauses() {
-    for literals in [vec![2], vec![-2], vec![2, -5], vec![-2, 5, 5]] {
-        let source = KSatisfiability::<K3>::new_allow_less(6, vec![CNFClause::new(literals)]);
+fn test_ksatisfiability_to_bicliquecover_normalization_preserves_repeated_literals() {
+    for literals in [
+        vec![2, 2, 2],
+        vec![-2, -2, -2],
+        vec![2, -5, -5],
+        vec![-2, 5, 5],
+    ] {
+        let source = KSatisfiability::<K3>::new(6, vec![CNFClause::new(literals)]);
         let reduction = ReduceTo::<BicliqueCover>::reduce_to(&source).unwrap();
         let (n, clauses) = super::normalize(&source, &reduction.source_variables).unwrap();
         let normalized =
diff --git a/src/unit_tests/rules/ksatisfiability_cyclicordering.rs b/src/unit_tests/rules/ksatisfiability_cyclicordering.rs
index 75c1ab6f7..078a004ae 100644
--- a/src/unit_tests/rules/ksatisfiability_cyclicordering.rs
+++ b/src/unit_tests/rules/ksatisfiability_cyclicordering.rs
@@ -207,22 +207,19 @@ fn test_ksatisfiability_to_cyclicordering_closed_loop() {
 }
 
 #[test]
-fn repeated_short_and_unsorted_clauses_preserve_all_source_assignments() {
+fn repeated_and_unsorted_clauses_preserve_all_source_assignments() {
     let formulas = [
         vec![vec![5, 5, 5]],
         vec![vec![-5, -5, -5]],
         vec![vec![5, -5, 5]],
         vec![vec![5, 2, 5]],
-        vec![vec![5]],
-        vec![vec![-5, 2]],
+        vec![vec![-5, 2, 2]],
         vec![vec![5, 1, -3], vec![-1, 5, 2], vec![-3, 2, -5]],
     ];
     for clauses in formulas {
-        let source = KSatisfiability::<K3>::try_new_allow_less(
-            6,
-            clauses.into_iter().map(CNFClause::new).collect(),
-        )
-        .unwrap();
+        let source =
+            KSatisfiability::<K3>::try_new(6, clauses.into_iter().map(CNFClause::new).collect())
+                .unwrap();
         let reduction = ReduceTo::<CyclicOrdering>::reduce_to(&source).unwrap();
         let normalized = normalize(&source).unwrap();
         assert!(normalized
@@ -248,7 +245,7 @@ fn repeated_short_and_unsorted_clauses_preserve_all_source_assignments() {
 }
 
 #[test]
-fn empty_formula_and_empty_clause_have_opposite_fixed_targets() {
+fn empty_formula_has_a_fixed_yes_target() {
     for num_vars in [0, 3] {
         let source = KSatisfiability::<K3>::new(num_vars, vec![]);
         let reduction = ReduceTo::<CyclicOrdering>::reduce_to(&source).unwrap();
@@ -257,22 +254,6 @@ fn empty_formula_and_empty_clause_have_opposite_fixed_targets() {
             reduction.extract_solution(&vec![0]).unwrap(),
             vec![false; num_vars]
         );
-        let source =
-            KSatisfiability::<K3>::try_new_allow_less(num_vars, vec![CNFClause::new(vec![])])
-                .unwrap();
-        let reduction = ReduceTo::<CyclicOrdering>::reduce_to(&source).unwrap();
-        assert_eq!(reduction.target_problem().num_elements(), 3);
-        for config in [
-            vec![0, 1, 2],
-            vec![0, 2, 1],
-            vec![1, 0, 2],
-            vec![1, 2, 0],
-            vec![2, 0, 1],
-            vec![2, 1, 0],
-        ] {
-            assert!(!reduction.target_problem().evaluate(&config).unwrap().0);
-            assert!(reduction.extract_solution(&config).is_err());
-        }
     }
 }
 
diff --git a/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs
index fc8d8f05d..4e42374c3 100644
--- a/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs
+++ b/src/unit_tests/rules/ksatisfiability_decisionminimumvertexcover.rs
@@ -88,30 +88,19 @@ fn test_ksatisfiability_to_decisionminimumvertexcover_extract_solution() {
 }
 
 #[test]
-fn test_ksatisfiability_to_decisionminimumvertexcover_short_clauses_closed_loop() {
-    let source = KSatisfiability::<K3>::new_allow_less(
+fn test_ksatisfiability_to_decisionminimumvertexcover_repeated_literals_closed_loop() {
+    let source = KSatisfiability::<K3>::new(
         2,
-        vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1, 2])],
+        vec![
+            CNFClause::new(vec![1, 1, 1]),
+            CNFClause::new(vec![-1, 2, 2]),
+        ],
     );
     let reduction =
         ReduceTo::<Decision<MinimumVertexCover<SimpleGraph, One>>>::reduce_to(&source).unwrap();
     assert_satisfaction_round_trip_from_satisfaction_target(
         &source,
         &reduction,
-        "short clauses -> Decision MVC",
+        "repeated literals -> Decision MVC",
     );
 }
-
-#[test]
-fn test_ksatisfiability_to_decisionminimumvertexcover_empty_clause() {
-    let source = KSatisfiability::<K3>::new_allow_less(0, vec![CNFClause::new(vec![])]);
-    let reduction =
-        ReduceTo::<Decision<MinimumVertexCover<SimpleGraph, One>>>::reduce_to(&source).unwrap();
-    assert_eq!(reduction.target_problem().bound(), &-1);
-    assert!(BruteForce::new().solve(&source).unwrap().is_none());
-    assert!(BruteForce::new()
-        .solve(reduction.target_problem())
-        .unwrap()
-        .is_none());
-    assert!(reduction.extract_solution(&vec![true; 3]).is_err());
-}
diff --git a/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs b/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs
index e242c81cf..5dffd13ee 100644
--- a/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs
+++ b/src/unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs
@@ -178,24 +178,8 @@ fn test_ksatisfiability_to_feasible_register_assignment_unsatisfiable_instance()
 }
 
 #[test]
-fn native_empty_clause_is_infeasible_and_empty_conjunction_is_feasible() {
+fn empty_conjunction_is_feasible() {
     for num_vars in [0, 3] {
-        let source =
-            KSatisfiability::<K3>::try_new_allow_less(num_vars, vec![CNFClause::new(vec![])])
-                .unwrap();
-        let reduction = ReduceTo::<FeasibleRegisterAssignment>::reduce_to(&source).unwrap();
-        assert_eq!(reduction.target_problem().num_vertices(), 3);
-        for config in [
-            vec![0, 1, 2],
-            vec![0, 2, 1],
-            vec![1, 0, 2],
-            vec![1, 2, 0],
-            vec![2, 0, 1],
-            vec![2, 1, 0],
-        ] {
-            assert!(!reduction.target_problem().evaluate(&config).unwrap().0);
-            assert!(reduction.extract_solution(&config).is_err());
-        }
         let source = KSatisfiability::<K3>::new(num_vars, vec![]);
         let reduction = ReduceTo::<FeasibleRegisterAssignment>::reduce_to(&source).unwrap();
         assert_eq!(reduction.target_problem().num_vertices(), 0);
@@ -207,21 +191,17 @@ fn native_empty_clause_is_infeasible_and_empty_conjunction_is_feasible() {
 }
 
 #[test]
-fn short_repeated_and_mixed_clauses_have_complete_forward_witnesses() {
+fn repeated_and_mixed_clauses_have_complete_forward_witnesses() {
     for formula in [
-        vec![vec![5]],
-        vec![vec![-5]],
-        vec![vec![5, 2]],
-        vec![vec![-5, 2]],
+        vec![vec![-5, -5, -5]],
+        vec![vec![-5, 2, 2]],
         vec![vec![5, 5, 5]],
         vec![vec![5, -5, 5]],
         vec![vec![5, 1, -3], vec![-1, 5, 2], vec![-3, 2, -5]],
     ] {
-        let source = KSatisfiability::<K3>::try_new_allow_less(
-            6,
-            formula.into_iter().map(CNFClause::new).collect(),
-        )
-        .unwrap();
+        let source =
+            KSatisfiability::<K3>::try_new(6, formula.into_iter().map(CNFClause::new).collect())
+                .unwrap();
         let reduction = ReduceTo::<FeasibleRegisterAssignment>::reduce_to(&source).unwrap();
         let a = reduction.source_variables.len();
         assert_eq!(
@@ -250,33 +230,6 @@ fn short_repeated_and_mixed_clauses_have_complete_forward_witnesses() {
     }
 }
 
-#[test]
-fn short_clause_padding_matches_its_equivalent_three_literal_formula() {
-    let short = KSatisfiability::<K3>::try_new_allow_less(
-        3,
-        vec![CNFClause::new(vec![3]), CNFClause::new(vec![-3])],
-    )
-    .unwrap();
-    let padded = KSatisfiability::<K3>::new(
-        3,
-        vec![
-            CNFClause::new(vec![3, 3, 3]),
-            CNFClause::new(vec![-3, -3, -3]),
-        ],
-    );
-    let a = ReduceTo::<FeasibleRegisterAssignment>::reduce_to(&short).unwrap();
-    let b = ReduceTo::<FeasibleRegisterAssignment>::reduce_to(&padded).unwrap();
-    assert_eq!(a.target_problem().arcs(), b.target_problem().arcs());
-    assert_eq!(
-        a.target_problem().assignment(),
-        b.target_problem().assignment()
-    );
-    assert_eq!(
-        a.target_problem().num_vertices(),
-        b.target_problem().num_vertices()
-    );
-}
-
 #[test]
 fn invalid_realizations_are_rejected() {
     let source = issue_example();
diff --git a/src/unit_tests/rules/ksatisfiability_kclique.rs b/src/unit_tests/rules/ksatisfiability_kclique.rs
index 0e0bf789b..baa3dc457 100644
--- a/src/unit_tests/rules/ksatisfiability_kclique.rs
+++ b/src/unit_tests/rules/ksatisfiability_kclique.rs
@@ -48,7 +48,7 @@ fn test_ksatisfiability_to_kclique_closed_loop() {
 }
 
 #[test]
-fn test_kclique_empty_formulas_and_short_clauses() {
+fn test_kclique_empty_formulas_and_repeated_literals() {
     for n in [0, 3, 4] {
         let source = KSatisfiability::<K3>::new(n, vec![]);
         let reduction = ReduceTo::<KClique<SimpleGraph>>::reduce_to(&source).unwrap();
@@ -65,16 +65,11 @@ fn test_kclique_empty_formulas_and_short_clauses() {
         );
     }
     for clauses in [
-        vec![vec![]],
-        vec![vec![], vec![]],
-        vec![vec![], vec![1]],
-        vec![vec![1], vec![-1]],
-        vec![vec![1], vec![2, -1]],
+        vec![vec![1, 1, 1], vec![-1, -1, -1]],
+        vec![vec![1, 1, 1], vec![2, -1, -1]],
     ] {
-        let source = KSatisfiability::<K3>::new_allow_less(
-            2,
-            clauses.into_iter().map(CNFClause::new).collect(),
-        );
+        let source =
+            KSatisfiability::<K3>::new(2, clauses.into_iter().map(CNFClause::new).collect());
         let reduction = ReduceTo::<KClique<SimpleGraph>>::reduce_to(&source).unwrap();
         let sat = BruteForce::new().solve(&source).unwrap().is_some();
         let solutions = BruteForce::new()
@@ -94,28 +89,25 @@ fn test_kclique_empty_formulas_and_short_clauses() {
 
 #[test]
 fn test_kclique_all_two_clause_formulas_and_target_selections() {
-    // All ordered clauses of width 0..3 on one variable, including repetitions
+    // All ordered three-literal clauses on one variable, including repetitions
     // and tautologies; every ordered pair and every raw target bitvector.
-    let mut clauses = vec![vec![]];
-    for width in 1..=3 {
-        for mask in 0..(1usize << width) {
-            clauses.push(
-                (0..width)
-                    .map(|p| if mask & (1 << p) == 0 { 1 } else { -1 })
-                    .collect(),
-            );
-        }
-    }
+    let clauses: Vec<Vec<i64>> = (0..8usize)
+        .map(|mask| {
+            (0..3)
+                .map(|p| if mask & (1 << p) == 0 { 1 } else { -1 })
+                .collect()
+        })
+        .collect();
     for a in &clauses {
         for b in &clauses {
-            let source = KSatisfiability::<K3>::new_allow_less(
+            let source = KSatisfiability::<K3>::new(
                 1,
                 vec![CNFClause::new(a.clone()), CNFClause::new(b.clone())],
             );
             let reduction = ReduceTo::<KClique<SimpleGraph>>::reduce_to(&source).unwrap();
             let target = reduction.target_problem();
             let t = a.len() + b.len();
-            assert_eq!(target.num_vertices(), t.max(2) + 1);
+            assert_eq!(target.num_vertices(), t + 1);
             assert_eq!(target.k(), 3);
             let mut source_yes = false;
             for value in [false, true] {
@@ -157,17 +149,20 @@ fn test_kclique_all_two_clause_formulas_and_target_selections() {
 
 #[test]
 fn test_kclique_rejects_malformed_or_non_clique_selections() {
-    let source = KSatisfiability::<K3>::new_allow_less(
+    let source = KSatisfiability::<K3>::new(
         3,
-        vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])],
+        vec![
+            CNFClause::new(vec![1, 2, 2]),
+            CNFClause::new(vec![-1, 3, 3]),
+        ],
     );
     let reduction = ReduceTo::<KClique<SimpleGraph>>::reduce_to(&source).unwrap();
     for bad in [
         vec![],
-        vec![true; 6],
-        vec![false; 5],
-        vec![true, true, false, false, true],
-        vec![true, false, true, false, true],
+        vec![true; 8],
+        vec![false; 7],
+        vec![true, true, false, false, false, false, true],
+        vec![true, false, false, true, false, false, true],
     ] {
         assert!(reduction.extract_solution(&bad).is_err());
     }
@@ -175,22 +170,17 @@ fn test_kclique_rejects_malformed_or_non_clique_selections() {
 
 #[test]
 fn test_kclique_count_boundaries() {
-    assert_eq!(clique_sizes(0, []).unwrap(), (1, 1));
-    assert_eq!(clique_sizes(3, [0, 0, 1]).unwrap(), (4, 4));
-    assert_eq!(clique_sizes(2, [3, 3]).unwrap(), (7, 3));
-    for (m, lengths) in [
-        (2, vec![usize::MAX, 1]),
-        (1, vec![usize::MAX]),
-        (usize::MAX, vec![]),
-    ] {
+    assert_eq!(clique_sizes(0).unwrap(), (1, 1));
+    assert_eq!(clique_sizes(2).unwrap(), (7, 3));
+    let largest = (usize::MAX - 1) / 3;
+    assert_eq!(
+        clique_sizes(largest).unwrap(),
+        (3 * largest + 1, largest + 1)
+    );
+    for m in [largest + 1, usize::MAX] {
         assert!(matches!(
-            clique_sizes(m, lengths),
+            clique_sizes(m),
             Err(crate::rules::ReductionError::IntegerOverflow { .. })
         ));
     }
-    assert_eq!(
-        clique_sizes(usize::MAX - 1, []).unwrap(),
-        (usize::MAX, usize::MAX)
-    );
-    assert_eq!(clique_sizes(1, [usize::MAX - 1]).unwrap(), (usize::MAX, 2));
 }
diff --git a/src/unit_tests/rules/ksatisfiability_kernel.rs b/src/unit_tests/rules/ksatisfiability_kernel.rs
index 200045a36..9805e42ac 100644
--- a/src/unit_tests/rules/ksatisfiability_kernel.rs
+++ b/src/unit_tests/rules/ksatisfiability_kernel.rs
@@ -79,18 +79,15 @@ fn test_ksatisfiability_to_kernel_extract_solution_reads_variable_gadgets() {
 }
 
 #[test]
-fn test_ksatisfiability_to_kernel_native_clause_domain() {
+fn test_ksatisfiability_to_kernel_one_variable_clause_domain() {
     use crate::traits::Problem;
-    let mut clauses = vec![vec![]];
-    for len in 1..=3 {
-        for mask in 0..(1 << len) {
-            clauses.push(
-                (0..len)
-                    .map(|j| if mask & (1 << j) == 0 { 1 } else { -1 })
-                    .collect(),
-            );
-        }
-    }
+    let clauses: Vec<Vec<i64>> = (0..8)
+        .map(|mask| {
+            (0..3)
+                .map(|j| if mask & (1 << j) == 0 { 1 } else { -1 })
+                .collect()
+        })
+        .collect();
     let mut formulas = vec![vec![]];
     for first in &clauses {
         formulas.push(vec![first.clone()]);
@@ -99,20 +96,16 @@ fn test_ksatisfiability_to_kernel_native_clause_domain() {
         }
     }
     for formula in formulas {
-        let source = KSatisfiability::<K3>::try_new_allow_less(
+        let source = KSatisfiability::<K3>::try_new(
             1,
             formula.iter().cloned().map(CNFClause::new).collect(),
         )
         .unwrap();
         let reduction = ReduceTo::<Kernel>::reduce_to(&source).unwrap();
         let target = reduction.target_problem();
-        let active = usize::from(formula.iter().any(|clause| !clause.is_empty()));
-        let occurrences: usize = formula.iter().map(Vec::len).sum();
+        let active = usize::from(!formula.is_empty());
         assert_eq!(target.num_vertices(), 2 * active + 3 * formula.len());
-        assert_eq!(
-            target.num_arcs(),
-            2 * active + 3 * formula.len() + occurrences
-        );
+        assert_eq!(target.num_arcs(), 2 * active + 6 * formula.len());
         let mut witnessed = [false; 2];
         for mask in 0..(1usize << target.num_vertices()) {
             let config = (0..target.num_vertices())
@@ -139,10 +132,14 @@ fn test_ksatisfiability_to_kernel_native_clause_domain() {
 #[test]
 fn test_ksatisfiability_to_kernel_sparse_inverse() {
     use crate::traits::Problem;
-    for literals in [vec![5], vec![-5], vec![5, -2], vec![5, -5, 2]] {
+    for literals in [
+        vec![5, 5, 5],
+        vec![-5, -5, -5],
+        vec![5, -2, -2],
+        vec![5, -5, 2],
+    ] {
         let source =
-            KSatisfiability::<K3>::try_new_allow_less(6, vec![CNFClause::new(literals.clone())])
-                .unwrap();
+            KSatisfiability::<K3>::try_new(6, vec![CNFClause::new(literals.clone())]).unwrap();
         let reduction = ReduceTo::<Kernel>::reduce_to(&source).unwrap();
         let target = reduction.target_problem();
         let mut found = false;
diff --git a/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs b/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs
index eaa8484bd..b70a1fc25 100644
--- a/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs
+++ b/src/unit_tests/rules/ksatisfiability_monochromatictriangle.rs
@@ -129,19 +129,16 @@ fn test_ksatisfiability_to_monochromatic_triangle_unsatisfiable_all_signs() {
 }
 
 #[test]
-fn test_ksatisfiability_to_monochromatic_triangle_short_and_repeated_literals() {
+fn test_ksatisfiability_to_monochromatic_triangle_repeated_literals() {
     for clauses in [
         vec![],
-        vec![vec![]],
-        vec![vec![1]],
-        vec![vec![1, -2]],
+        vec![vec![1, 1, 1]],
+        vec![vec![1, -2, -2]],
         vec![vec![1, 1, 1], vec![-1, -1, -1]],
         vec![vec![1, -1, 2]],
     ] {
-        let source = KSatisfiability::<K3>::new_allow_less(
-            3,
-            clauses.into_iter().map(CNFClause::new).collect(),
-        );
+        let source =
+            KSatisfiability::<K3>::new(3, clauses.into_iter().map(CNFClause::new).collect());
         let feasible = (0..8).any(|bits| {
             source
                 .evaluate(&(0..3).map(|i| bits & (1 << i) != 0).collect())
diff --git a/src/unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs
index 5792a4456..b9d92bce7 100644
--- a/src/unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs
+++ b/src/unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs
@@ -110,18 +110,16 @@ fn test_ksatisfiability_to_oneinthreesatisfiability_extract_solution() {
 }
 
 #[test]
-fn test_oneinthree_native_empty_short_and_sparse_clauses() {
+fn test_oneinthree_empty_repeated_and_sparse_clauses() {
     for (num_vars, formula) in [
         (0, vec![]),
         (3, vec![]),
-        (0, vec![vec![]]),
-        (3, vec![vec![]]),
-        (5, vec![vec![5]]),
-        (5, vec![vec![-5]]),
-        (5, vec![vec![5, -2]]),
+        (5, vec![vec![5, 5, 5]]),
+        (5, vec![vec![-5, -5, -5]]),
+        (5, vec![vec![5, -2, -2]]),
         (5, vec![vec![5, -5, 2]]),
     ] {
-        let source = KSatisfiability::<K3>::try_new_allow_less(
+        let source = KSatisfiability::<K3>::try_new(
             num_vars,
             formula.iter().cloned().map(CNFClause::new).collect(),
         )
diff --git a/src/unit_tests/rules/ksatisfiability_preemptivescheduling.rs b/src/unit_tests/rules/ksatisfiability_preemptivescheduling.rs
index 6fb987b1a..25c7c3e93 100644
--- a/src/unit_tests/rules/ksatisfiability_preemptivescheduling.rs
+++ b/src/unit_tests/rules/ksatisfiability_preemptivescheduling.rs
@@ -142,20 +142,15 @@ fn test_ksatisfiability_to_preemptivescheduling_unsatisfiable_threshold_gap() {
 }
 
 #[test]
-fn test_threshold_value_mapping_and_short_clauses() {
+fn test_threshold_value_mapping_and_repeated_literals() {
     use crate::rules::AggregateReductionResult;
     use crate::types::Or;
 
     for source in [
         KSatisfiability::<K3>::new(0, vec![]),
         KSatisfiability::<K3>::new(2, vec![]),
-        KSatisfiability::<K3>::new_allow_less(0, vec![CNFClause::new(vec![])]),
-        KSatisfiability::<K3>::new_allow_less(1, vec![CNFClause::new(vec![1])]),
-        KSatisfiability::<K3>::new_allow_less(2, vec![CNFClause::new(vec![1, -2])]),
-        KSatisfiability::<K3>::new_allow_less(
-            1,
-            vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
-        ),
+        KSatisfiability::<K3>::new(1, vec![CNFClause::new(vec![1, 1, 1])]),
+        KSatisfiability::<K3>::new(2, vec![CNFClause::new(vec![1, -2, -2])]),
         yes_single_variable_instance(),
         no_single_variable_instance(),
     ] {
@@ -238,14 +233,22 @@ fn test_registered_aggregate_mapping() {
                 && edge.target_name == "PreemptiveScheduling"
         })
         .unwrap();
-    for (clauses, expected) in [(vec![], true), (vec![CNFClause::new(vec![])], false)] {
-        let source = KSatisfiability::<K3>::new_allow_less(0, clauses);
-        let result = (edge.reduce_aggregate_fn.unwrap())(&source).unwrap();
-        assert_eq!(
-            result
-                .extract_value_from_solution_dyn(&vec![vec![true]])
-                .unwrap(),
-            serde_json::json!(expected),
-        );
-    }
+    let yes = KSatisfiability::<K3>::new(0, vec![]);
+    let result = (edge.reduce_aggregate_fn.unwrap())(&yes).unwrap();
+    assert_eq!(
+        result
+            .extract_value_from_solution_dyn(&vec![vec![true]])
+            .unwrap(),
+        serde_json::json!(true),
+    );
+    // An all-idle schedule leaves every task unfinished, so it is never feasible.
+    let no = no_single_variable_instance();
+    let target = ReduceTo::<PreemptiveScheduling>::reduce_to(&no).unwrap();
+    let target = ReductionResult::target_problem(&target);
+    let idle = vec![vec![false; target.d_max()]; target.num_tasks()];
+    let result = (edge.reduce_aggregate_fn.unwrap())(&no).unwrap();
+    assert_eq!(
+        result.extract_value_from_solution_dyn(&idle).unwrap(),
+        serde_json::json!(false),
+    );
 }
diff --git a/src/unit_tests/rules/ksatisfiability_quadraticcongruences.rs b/src/unit_tests/rules/ksatisfiability_quadraticcongruences.rs
index 098a88b18..94b893ba2 100644
--- a/src/unit_tests/rules/ksatisfiability_quadraticcongruences.rs
+++ b/src/unit_tests/rules/ksatisfiability_quadraticcongruences.rs
@@ -6,8 +6,7 @@ use crate::types::Or;
 use num_traits::ToPrimitive;
 
 fn source(n: usize, clauses: Vec<Vec<i64>>) -> KSatisfiability<K3> {
-    KSatisfiability::try_new_allow_less(n, clauses.into_iter().map(CNFClause::new).collect())
-        .unwrap()
+    KSatisfiability::new(n, clauses.into_iter().map(CNFClause::new).collect())
 }
 
 #[test]
@@ -35,15 +34,13 @@ fn test_ksatisfiability_to_quadraticcongruences_closed_loop() {
 fn test_native_clauses_and_arbitrary_crt_signs() {
     for source in [
         source(0, vec![]),
-        source(0, vec![vec![]]),
         source(3, vec![vec![1, 1, 1]]),
         source(3, vec![vec![-1, -1, -1]]),
-        source(3, vec![vec![1, 2]]),
+        source(3, vec![vec![1, 2, 2]]),
         source(3, vec![vec![1, 2, 3]]),
         source(3, vec![vec![-3, -1, 2]]),
-        source(2, vec![vec![1], vec![-1]]),
-        source(2, vec![vec![1, 2], vec![-1, -2]]),
-        source(2, vec![vec![], vec![1, 2]]),
+        source(2, vec![vec![1, 1, 1], vec![-1, -1, -1]]),
+        source(2, vec![vec![1, 2, 2], vec![-1, -2, -2]]),
         source(17, vec![vec![17, 17, 17]]),
     ] {
         let construction = build_construction(&source).unwrap();
@@ -146,7 +143,7 @@ fn test_unsatisfiable_formula_has_no_quadratic_sign_witness() {
 
 #[test]
 fn test_normalization_preserves_free_variables_and_formula() {
-    let canonical = source(5, vec![vec![-5, 2]]);
+    let canonical = source(5, vec![vec![-5, 2, 2]]);
     let redundant = source(5, vec![vec![2, -5, 2], vec![-5, 2, -5], vec![1, -1, 4]]);
     let first = ReduceTo::<QuadraticCongruences>::reduce_to(&canonical).unwrap();
     let second = ReduceTo::<QuadraticCongruences>::reduce_to(&redundant).unwrap();
@@ -200,9 +197,8 @@ fn test_prime_generation_and_parameter_bounds() {
     assert_eq!(admissible_primes(4).unwrap(), vec![13, 17, 19, 23]);
     for source in [
         source(0, vec![]),
-        source(0, vec![vec![]]),
         source(3, vec![vec![1, 2, 3]]),
-        source(1, vec![vec![1], vec![-1]]),
+        source(1, vec![vec![1, 1, 1], vec![-1, -1, -1]]),
     ] {
         let reduction = ReduceTo::<QuadraticCongruences>::reduce_to(&source).unwrap();
         let n = 2 * source.num_clauses() + source.num_vars() + 1;
diff --git a/src/unit_tests/rules/ksatisfiability_qubo.rs b/src/unit_tests/rules/ksatisfiability_qubo.rs
index 2d9aae200..4a03d7869 100644
--- a/src/unit_tests/rules/ksatisfiability_qubo.rs
+++ b/src/unit_tests/rules/ksatisfiability_qubo.rs
@@ -234,24 +234,21 @@ fn test_k3satisfiability_to_qubo_all_negated() {
 }
 
 #[test]
-fn test_sat_qubo_all_short_clauses_and_raw_targets() {
+fn test_sat_qubo_all_one_variable_clause_pairs_and_raw_targets() {
     use crate::rules::AggregateReductionResult;
     use crate::types::{Min, Or};
     macro_rules! verify {
         ($k:ty, $width:expr) => {{
-            let mut clauses = vec![vec![]];
-            for width in 1..=$width {
-                for mask in 0..(1 << width) {
-                    clauses.push(
-                        (0..width)
-                            .map(|p| if mask & (1 << p) == 0 { 1 } else { -1 })
-                            .collect(),
-                    );
-                }
-            }
+            let clauses: Vec<Vec<i64>> = (0..1 << $width)
+                .map(|mask| {
+                    (0..$width)
+                        .map(|p| if mask & (1 << p) == 0 { 1 } else { -1 })
+                        .collect()
+                })
+                .collect();
             for a in &clauses {
                 for b in &clauses {
-                    let source = KSatisfiability::<$k>::new_allow_less(
+                    let source = KSatisfiability::<$k>::new(
                         1,
                         vec![CNFClause::new(a.clone()), CNFClause::new(b.clone())],
                     );
@@ -270,8 +267,6 @@ fn test_sat_qubo_all_short_clauses_and_raw_targets() {
                                 .map(|&l| i64::from(witness[0] != (l > 0)))
                                 .collect();
                             penalty += match y.as_slice() {
-                                [] => 1,
-                                &[u] => u,
                                 &[u, v] => u * v,
                                 &[u, v, w] => {
                                     let z = i64::from(witness[1 + j]);
@@ -363,9 +358,12 @@ fn test_sat_qubo_checked_numeric_boundaries() {
 #[test]
 fn test_sat_qubo_registered_aggregate_threshold() {
     macro_rules! check {
-        ($k:ty) => {
-            for (clauses, expected) in [(vec![vec![1]], true), (vec![vec![1], vec![-1]], false)] {
-                let source = KSatisfiability::<$k>::new_allow_less(
+        ($k:ty, $width:expr) => {
+            for (clauses, expected) in [
+                (vec![vec![1; $width]], true),
+                (vec![vec![1; $width], vec![-1; $width]], false),
+            ] {
+                let source = KSatisfiability::<$k>::new(
                     1,
                     clauses.into_iter().map(CNFClause::new).collect(),
                 );
@@ -390,6 +388,6 @@ fn test_sat_qubo_registered_aggregate_threshold() {
             }
         };
     }
-    check!(K2);
-    check!(K3);
+    check!(K2, 2);
+    check!(K3, 3);
 }
diff --git a/src/unit_tests/rules/ksatisfiability_registersufficiency.rs b/src/unit_tests/rules/ksatisfiability_registersufficiency.rs
index 301cf7af3..e9a2fbced 100644
--- a/src/unit_tests/rules/ksatisfiability_registersufficiency.rs
+++ b/src/unit_tests/rules/ksatisfiability_registersufficiency.rs
@@ -148,77 +148,66 @@ fn test_ksatisfiability_to_register_sufficiency_canonical_example_spec() {
 }
 
 #[test]
-fn test_ksatisfiability_to_registersufficiency_closed_loop_boundaries() {
+fn test_ksatisfiability_to_registersufficiency_empty_formula() {
     use crate::solvers::BruteForce;
     for declared in [0, 5] {
-        let yes = KSatisfiability::<K3>::new(declared, vec![]);
-        let no = KSatisfiability::<K3>::try_new_allow_less(declared, vec![CNFClause::new(vec![])])
+        let source = KSatisfiability::<K3>::new(declared, vec![]);
+        let reduction = ReduceTo::<RegisterSufficiency>::reduce_to(&source).unwrap();
+        let solution = BruteForce::new()
+            .solve(reduction.target_problem())
+            .unwrap()
             .unwrap();
-        for (source, feasible) in [(yes, true), (no, false)] {
-            let reduction = ReduceTo::<RegisterSufficiency>::reduce_to(&source).unwrap();
-            let solution = BruteForce::new().solve(reduction.target_problem()).unwrap();
-            assert_eq!(solution.is_some(), feasible);
-            if let Some(solution) = solution {
-                let extracted = reduction.extract_solution(&solution).unwrap();
-                assert_eq!(extracted, vec![false; declared]);
-                assert_eq!(source.evaluate(&extracted).unwrap(), Or(true));
-            } else {
-                assert!(reduction.extract_solution(&vec![0]).is_err());
-            }
-        }
+        let extracted = reduction.extract_solution(&solution).unwrap();
+        assert_eq!(extracted, vec![false; declared]);
+        assert_eq!(source.evaluate(&extracted).unwrap(), Or(true));
     }
 }
 
 #[test]
-fn test_short_repeated_and_tautological_clauses() {
+fn test_repeated_and_tautological_clauses() {
     for num_vars in 1..=3 {
         let literals: Vec<i64> = (1..=num_vars)
             .flat_map(|i| [i as i64, -(i as i64)])
             .collect();
-        for width in 1..=3 {
-            for code in 0..literals.len().pow(width) {
-                let mut remaining = code;
-                let clause: Vec<_> = (0..width)
-                    .map(|_| {
-                        let lit = literals[remaining % literals.len()];
-                        remaining /= literals.len();
-                        lit
-                    })
+        for code in 0..literals.len().pow(3) {
+            let mut remaining = code;
+            let clause: Vec<_> = (0..3)
+                .map(|_| {
+                    let lit = literals[remaining % literals.len()];
+                    remaining /= literals.len();
+                    lit
+                })
+                .collect();
+            let source =
+                KSatisfiability::<K3>::try_new(num_vars, vec![CNFClause::new(clause)]).unwrap();
+            let reduction = ReduceTo::<RegisterSufficiency>::reduce_to(&source).unwrap();
+            let layout = reduction.layout.as_ref().unwrap();
+            for mask in 0..(1usize << num_vars) {
+                let original: Vec<_> = (0..num_vars).map(|i| mask & (1 << i) != 0).collect();
+                let compact: Vec<_> = reduction
+                    .source_variables
+                    .iter()
+                    .map(|&i| original[i])
                     .collect();
-                let source = KSatisfiability::<K3>::try_new_allow_less(
-                    num_vars,
-                    vec![CNFClause::new(clause)],
-                )
-                .unwrap();
-                let reduction = ReduceTo::<RegisterSufficiency>::reduce_to(&source).unwrap();
-                let layout = reduction.layout.as_ref().unwrap();
-                for mask in 0..(1usize << num_vars) {
-                    let original: Vec<_> = (0..num_vars).map(|i| mask & (1 << i) != 0).collect();
-                    let compact: Vec<_> = reduction
-                        .source_variables
-                        .iter()
-                        .map(|&i| original[i])
-                        .collect();
-                    let positions = layout.schedule_for_assignment(&compact);
-                    assert!(reduction
-                        .target_problem()
-                        .simulate_registers(&positions)
-                        .unwrap()
-                        .is_some());
-                    let source_value = source.evaluate(&original).unwrap();
-                    assert_eq!(
-                        reduction.target_problem().evaluate(&positions).unwrap(),
-                        source_value
-                    );
-                    if source_value.0 {
-                        let decoded = reduction.extract_solution(&positions).unwrap();
-                        assert_eq!(source.evaluate(&decoded).unwrap(), Or(true));
-                        for &i in &reduction.source_variables {
-                            assert_eq!(decoded[i], original[i]);
-                        }
-                    } else {
-                        assert!(reduction.extract_solution(&positions).is_err());
+                let positions = layout.schedule_for_assignment(&compact);
+                assert!(reduction
+                    .target_problem()
+                    .simulate_registers(&positions)
+                    .unwrap()
+                    .is_some());
+                let source_value = source.evaluate(&original).unwrap();
+                assert_eq!(
+                    reduction.target_problem().evaluate(&positions).unwrap(),
+                    source_value
+                );
+                if source_value.0 {
+                    let decoded = reduction.extract_solution(&positions).unwrap();
+                    assert_eq!(source.evaluate(&decoded).unwrap(), Or(true));
+                    for &i in &reduction.source_variables {
+                        assert_eq!(decoded[i], original[i]);
                     }
+                } else {
+                    assert!(reduction.extract_solution(&positions).is_err());
                 }
             }
         }
@@ -227,8 +216,7 @@ fn test_short_repeated_and_tautological_clauses() {
 
 #[test]
 fn test_sparse_original_variables_and_padding_bound() {
-    let source =
-        KSatisfiability::<K3>::try_new_allow_less(17, vec![CNFClause::new(vec![-17, 2])]).unwrap();
+    let source = KSatisfiability::<K3>::new(17, vec![CNFClause::new(vec![-17, 2, 2])]);
     let reduction = ReduceTo::<RegisterSufficiency>::reduce_to(&source).unwrap();
     assert_eq!(reduction.source_variables, vec![1, 16]);
     let layout = reduction.layout.as_ref().unwrap();
diff --git a/src/unit_tests/rules/ksatisfiability_timetabledesign.rs b/src/unit_tests/rules/ksatisfiability_timetabledesign.rs
index ea24af2bd..6daf8db98 100644
--- a/src/unit_tests/rules/ksatisfiability_timetabledesign.rs
+++ b/src/unit_tests/rules/ksatisfiability_timetabledesign.rs
@@ -18,9 +18,12 @@ fn satisfiable_instance() -> KSatisfiability<K3> {
 }
 
 fn unsatisfiable_instance() -> KSatisfiability<K3> {
-    KSatisfiability::<K3>::new_allow_less(
+    KSatisfiability::<K3>::new(
         1,
-        vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])],
+        vec![
+            CNFClause::new(vec![1, 1, 1]),
+            CNFClause::new(vec![-1, -1, -1]),
+        ],
     )
 }
 
diff --git a/src/unit_tests/rules/maxcut_minimummatrixcover.rs b/src/unit_tests/rules/maxcut_minimummatrixcover.rs
index 7e6ef4a1b..78a7acd48 100644
--- a/src/unit_tests/rules/maxcut_minimummatrixcover.rs
+++ b/src/unit_tests/rules/maxcut_minimummatrixcover.rs
@@ -229,7 +229,7 @@ fn test_empty_graph() {
 
 #[test]
 fn test_overhead_num_rows_equals_num_vertices() {
-    // Spot-check the exact parameter relation: target.num_rows == source.num_vertices.
+    // Nonnegative weights add no auxiliary rows.
     for n in [1usize, 2, 5, 8] {
         let edges: Vec<(usize, usize)> = (0..n.saturating_sub(1)).map(|i| (i, i + 1)).collect();
         let weights: Vec<i64> = vec![1; edges.len()];
@@ -241,12 +241,98 @@ fn test_overhead_num_rows_equals_num_vertices() {
 }
 
 #[test]
-fn test_negative_weight_is_rejected() {
-    // The reduction only handles nonnegative weights.
-    let source = MaxCut::<SimpleGraph, i64>::new(SimpleGraph::new(2, vec![(0, 1)]), vec![-1]);
+fn test_maxcut_to_minimummatrixcover_closed_loop_negative_weights() {
+    // Mixed signs: a negative edge rewards keeping its endpoints together.
+    for (n, edges, weights) in [
+        (2, vec![(0, 1)], vec![-1_i64]),
+        (3, vec![(0, 1), (1, 2), (0, 2)], vec![-2, 3, 1]),
+        (4, vec![(0, 1), (1, 2), (2, 3), (0, 3)], vec![-1, -1, 2, 2]),
+        (3, vec![(0, 1), (1, 2), (0, 2)], vec![-1, -1, -1]),
+    ] {
+        let source = MaxCut::<SimpleGraph, i64>::new(SimpleGraph::new(n, edges), weights);
+        let reduction =
+            ReduceTo::<MinimumMatrixCover>::reduce_to(&source).expect("reduction should succeed");
+        assert_optimization_round_trip_from_optimization_target(
+            &source,
+            &reduction,
+            "MaxCut with negative weights -> MinimumMatrixCover",
+        );
+    }
+}
+
+#[test]
+fn test_negative_edge_gadget_layout() {
+    // Edge {0, 1} with w = -2 adds vertex 2: weight 3 to v = 1 and 2 to u = 0.
+    let source = MaxCut::<SimpleGraph, i64>::new(SimpleGraph::new(2, vec![(0, 1)]), vec![-2]);
+    let reduction =
+        ReduceTo::<MinimumMatrixCover>::reduce_to(&source).expect("reduction should succeed");
+    let expected: Vec<Vec<i64>> = vec![vec![0, 0, 2], vec![0, 0, 3], vec![2, 3, 0]];
+    assert_eq!(reduction.target_problem().matrix(), expected.as_slice());
+    // Auxiliary bits are dropped on extraction.
+    assert_eq!(
+        reduction
+            .extract_solution(&vec![true, true, false])
+            .unwrap(),
+        vec![true, true]
+    );
+}
+
+#[test]
+fn test_minimum_negative_weight_overflows() {
+    let source = MaxCut::<SimpleGraph, i64>::new(SimpleGraph::new(2, vec![(0, 1)]), vec![i64::MIN]);
     let error = ReduceTo::<MinimumMatrixCover>::reduce_to(&source).unwrap_err();
     assert!(matches!(
         error,
-        crate::rules::ReductionError::InvalidTarget { .. }
+        crate::rules::ReductionError::IntegerOverflow { .. }
     ));
 }
+
+#[test]
+fn test_unrepresentable_matrix_objective_is_rejected() {
+    for (n, edges, weights) in [
+        (2, vec![(0, 1)], vec![-3_000_000_000_000_000_000]),
+        (2, vec![(0, 1)], vec![-((i64::MAX - 2) / 4 + 1)]),
+        (2, vec![(0, 1)], vec![i64::MAX / 2 + 1]),
+        (3, vec![(0, 1), (1, 2)], vec![-2_000_000_000_000_000_000; 2]),
+        (
+            3,
+            vec![(0, 1), (1, 2)],
+            vec![-1_000_000_000_000_000_000, 3_000_000_000_000_000_000],
+        ),
+    ] {
+        let source = MaxCut::<SimpleGraph, i64>::new(SimpleGraph::new(n, edges), weights);
+        // Every source configuration is evaluable, including its optimum.
+        let optimum = BruteForce::new().solve(&source).unwrap().unwrap();
+        assert!(source.evaluate(&optimum).unwrap().0.is_some());
+        assert!(matches!(
+            ReduceTo::<MinimumMatrixCover>::reduce_to(&source),
+            Err(crate::rules::ReductionError::IntegerOverflow { .. })
+        ));
+    }
+}
+
+#[test]
+fn test_representable_matrix_objective_boundaries() {
+    for (weight, expected) in [(-((i64::MAX - 2) / 4), 0), (i64::MAX / 2, i64::MAX / 2)] {
+        let source =
+            MaxCut::<SimpleGraph, i64>::new(SimpleGraph::new(2, vec![(0, 1)]), vec![weight]);
+        let reduction = ReduceTo::<MinimumMatrixCover>::reduce_to(&source).unwrap();
+        assert_optimization_round_trip_from_optimization_target(
+            &source,
+            &reduction,
+            "MaxCut at the matrix objective boundary",
+        );
+        let target = reduction.target_problem();
+        assert_eq!(
+            target.evaluate(&vec![false; target.num_rows()]).unwrap(),
+            Min(Some(i64::MAX - 1))
+        );
+        let target_optimum = BruteForce::new().solve(target).unwrap().unwrap();
+        assert_eq!(
+            target.evaluate(&target_optimum).unwrap(),
+            Min(Some(-(i64::MAX - 1)))
+        );
+        let extracted = reduction.extract_solution(&target_optimum).unwrap();
+        assert_eq!(source.evaluate(&extracted).unwrap(), Max(Some(expected)));
+    }
+}
diff --git a/src/unit_tests/symbolic_parameter_contracts.rs b/src/unit_tests/symbolic_parameter_contracts.rs
index a7e6bfb34..c881b99c7 100644
--- a/src/unit_tests/symbolic_parameter_contracts.rs
+++ b/src/unit_tests/symbolic_parameter_contracts.rs
@@ -587,10 +587,11 @@ fn missing_structural_bounds_cover_sparse_and_normalized_instances() {
         SimpleGraph::path(3),
         SimpleGraph::complete(3),
     ] {
+        // SimpleGraph rejects repeated edges, so the bipartite side sizes are exact.
         check_reduced_parameters::<_, BalancedCompleteBipartiteSubgraph>(
             KClique::new(graph, 2),
             &["num_vertices"],
-            upper,
+            ParameterRelation::Exact,
         );
     }
 }
@@ -683,12 +684,8 @@ fn sat_flow_and_scheduling_bounds_cover_fixed_outputs() {
         misc::PreemptiveScheduling,
     };
     use crate::variant::K3;
-    for clauses in [
-        vec![],
-        vec![CNFClause::new(vec![])],
-        vec![CNFClause::new(vec![1, 1, -2])],
-    ] {
-        let source = KSatisfiability::<K3>::new_allow_less(2, clauses);
+    for clauses in [vec![], vec![CNFClause::new(vec![1, 1, -2])]] {
+        let source = KSatisfiability::<K3>::new(2, clauses);
         check_reduced_parameters::<_, DirectedTwoCommodityIntegralFlow>(
             source.clone(),
             &["max_capacity"],
@@ -932,3 +929,127 @@ fn vertex_cover_lcs_transition_bounds_cover_empty_strings() {
         );
     }
 }
+
+#[test]
+fn three_sat_counts_are_exact_on_repeated_literals() {
+    use crate::models::decision::Decision;
+    use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability};
+    use crate::models::graph::{KClique, MinimumVertexCover, MonochromaticTriangle};
+    use crate::models::misc::SubsetSum;
+    use crate::types::One;
+    use crate::variant::K3;
+    let exact = ParameterRelation::Exact;
+    for clauses in [
+        vec![],
+        vec![CNFClause::new(vec![1, 1, 1])],
+        vec![
+            CNFClause::new(vec![1, -2, -2]),
+            CNFClause::new(vec![2, 2, 2]),
+        ],
+    ] {
+        let source = KSatisfiability::<K3>::new(2, clauses);
+        check_reduced_parameters::<_, KClique<SimpleGraph>>(
+            source.clone(),
+            &["k", "num_vertices"],
+            exact,
+        );
+        check_reduced_parameters::<_, Decision<MinimumVertexCover<SimpleGraph, One>>>(
+            source.clone(),
+            &["num_vertices", "num_edges"],
+            exact,
+        );
+        check_reduced_parameters::<_, OneInThreeSatisfiability>(
+            source.clone(),
+            &["num_clauses"],
+            exact,
+        );
+        check_reduced_parameters::<_, MonochromaticTriangle<SimpleGraph>>(
+            source.clone(),
+            &["num_vertices", "num_edges", "num_triangles"],
+            exact,
+        );
+        check_reduced_parameters::<_, SubsetSum>(source, &["num_elements"], exact);
+    }
+}
+
+#[test]
+fn exact_construction_counts_hold_on_degenerate_graphs() {
+    use crate::models::algebraic::ILP;
+    use crate::models::decision::Decision;
+    use crate::models::graph::{
+        HamiltonianCircuit, Kernel, MaximalIS, MaximumMatching, MinimumCoveringByCliques,
+        MinimumDominatingSet, MinimumVertexCover, PartitionIntoCliques,
+        PartitionIntoPathsOfLength2, PartitionIntoPerfectMatchings,
+    };
+    use crate::models::misc::EnsembleComputation;
+    use crate::topology::{Graph, SimpleDigraph};
+    use crate::types::One;
+    // Canonical examples are mid-sized; check the boundaries exact claims rely on:
+    // no vertices, no edges, and every valid k.
+    let exact = ParameterRelation::Exact;
+    for n in 0..=3 {
+        for graph in [
+            SimpleGraph::empty(n),
+            SimpleGraph::path(n),
+            SimpleGraph::complete(n),
+        ] {
+            let m = graph.num_edges();
+            check_reduced_parameters::<_, ILP<i64, i64, Bounded>>(
+                HamiltonianCircuit::new(graph.clone()),
+                &["num_vars", "num_nonzeros"],
+                exact,
+            );
+            check_reduced_parameters::<_, ILP<bool>>(
+                MaximalIS::new(graph.clone(), vec![1_i64; n]),
+                &["num_constraints", "num_nonzeros"],
+                exact,
+            );
+            check_reduced_parameters::<_, ILP<bool>>(
+                MinimumDominatingSet::new(graph.clone(), vec![1_i64; n]),
+                &["num_nonzeros"],
+                exact,
+            );
+            check_reduced_parameters::<_, ILP<bool>>(
+                MaximumMatching::new(graph.clone(), vec![1_i64; m]),
+                &["num_nonzeros"],
+                exact,
+            );
+            check_reduced_parameters::<_, EnsembleComputation>(
+                MinimumVertexCover::new(graph.clone(), vec![One; n]),
+                &["universe_size", "num_subsets"],
+                exact,
+            );
+            for k in 1..=n {
+                check_reduced_parameters::<_, ILP<i64, i64, Bounded>>(
+                    PartitionIntoPerfectMatchings::new(graph.clone(), k),
+                    &["num_vars", "num_constraints"],
+                    exact,
+                );
+                check_reduced_parameters::<_, Decision<MinimumCoveringByCliques<SimpleGraph>>>(
+                    PartitionIntoCliques::new(graph.clone(), k),
+                    &["num_vertices", "num_edges"],
+                    exact,
+                );
+            }
+            if n % 3 == 0 {
+                check_reduced_parameters::<_, ILP<bool>>(
+                    PartitionIntoPathsOfLength2::new(graph.clone()),
+                    &["num_vars", "num_constraints", "num_nonzeros"],
+                    exact,
+                );
+            }
+        }
+    }
+    for arcs in [
+        vec![],
+        vec![(0, 1)],
+        vec![(0, 1), (1, 0)],
+        vec![(0, 1), (1, 2), (2, 0)],
+    ] {
+        check_reduced_parameters::<_, ILP<bool>>(
+            Kernel::new(SimpleDigraph::new(3, arcs)),
+            &["num_nonzeros"],
+            exact,
+        );
+    }
+}