From 578078633b9744597666cd75272fe5b15fcfb047 Mon Sep 17 00:00:00 2001
From: Xiwei Pan <xiwei.pan@connect.hkust-gz.edu.cn>
Date: Fri, 7 Aug 2026 02:14:43 +0800
Subject: [PATCH 1/5] Establish numeric types and arithmetic standard

---
 .claude/CLAUDE.md                             |  10 ++
 .claude/skills/add-model/SKILL.md             |   2 +
 .claude/skills/add-rule/SKILL.md              |   9 ++
 .claude/skills/review-structural/SKILL.md     |   4 +
 .github/ISSUE_TEMPLATE/problem.md             |  12 ++
 .github/ISSUE_TEMPLATE/rule.md                |  12 ++
 docs/src/design.md                            |  90 +++++++++++++
 problemreductions-cli/src/commands/create.rs  |   8 +-
 .../src/commands/create/schema_support.rs     |   2 +-
 src/models/formula/ksat.rs                    |  69 +++++++---
 .../formula/maximum_2_satisfiability.rs       |  37 +++--
 src/models/formula/mod.rs                     |   1 +
 src/models/formula/nae_satisfiability.rs      |   3 +-
 .../formula/one_in_three_satisfiability.rs    |  46 ++++---
 src/models/formula/planar_3_satisfiability.rs |  46 ++++---
 src/models/formula/qbf.rs                     |  45 +++++--
 src/models/formula/sat.rs                     | 127 +++++++++++++++++-
 src/models/graph/mixed_chinese_postman.rs     |  18 +--
 src/rules/circuit_sat.rs                      |  23 ++--
 ...overby3sets_boundeddiameterspanningtree.rs |   7 +-
 ...oniancircuit_biconnectivityaugmentation.rs |   3 +-
 ...ncircuit_strongconnectivityaugmentation.rs |   3 +-
 src/rules/ksatisfiability_acyclicpartition.rs |  16 +--
 ...tisfiability_decisionminimumvertexcover.rs |   8 +-
 ...satisfiability_oneinthreesatisfiability.rs |  53 +++++---
 src/rules/ksatisfiability_timetabledesign.rs  |  46 ++++---
 ...nimumvertexcover_comparativecontainment.rs |   3 +-
 src/rules/sat_ksat.rs                         |  37 +++--
 .../satisfiability_maximum2satisfiability.rs  |  46 ++++---
 src/rules/satisfiability_naesatisfiability.rs |  11 +-
 src/solvers/decision_search.rs                |  22 +--
 src/types.rs                                  |  17 +--
 .../formula/one_in_three_satisfiability.rs    |   2 +-
 .../models/formula/planar_3_satisfiability.rs |   2 +-
 src/unit_tests/models/formula/qbf.rs          |   4 +-
 src/unit_tests/models/formula/sat.rs          |  29 +++-
 src/unit_tests/models/graph/max_cut.rs        |   2 +-
 src/unit_tests/models/graph/maximal_is.rs     |   2 +-
 .../models/graph/maximum_independent_set.rs   |   2 +-
 .../models/graph/maximum_matching.rs          |   2 +-
 .../models/graph/minimum_dominating_set.rs    |   2 +-
 .../models/graph/minimum_vertex_cover.rs      |   2 +-
 src/unit_tests/models/graph/spin_glass.rs     |   2 +-
 .../models/set/maximum_set_packing.rs         |   2 +-
 .../models/set/minimum_set_covering.rs        |   2 +-
 ...imumdominatingset_minimumsummulticenter.rs |   5 +-
 ...nminimumdominatingset_minmaxmulticenter.rs |   2 +-
 ...onminimumvertexcover_hamiltoniancircuit.rs |   2 +-
 ...overby3sets_boundeddiameterspanningtree.rs |   2 +-
 .../rules/hamiltoniancircuit_ruralpostman.rs  |   2 +-
 .../rules/maxcut_minimummatrixcover.rs        |   2 +-
 .../rules/maximum2satisfiability_maxcut.rs    |   2 +-
 ...nimumvertexcover_comparativecontainment.rs |   2 +-
 src/unit_tests/rules/sat_ksat.rs              |   4 +-
 tests/main.rs                                 |   2 +
 tests/suites/numeric_boundaries.rs            | 104 ++++++++++++++
 56 files changed, 770 insertions(+), 250 deletions(-)
 create mode 100644 tests/suites/numeric_boundaries.rs

diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 502e837f5..c15470b14 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -214,6 +214,16 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
 
 ## Conventions
 
+### Numeric Contract
+
+Follow the [numeric types and arithmetic standard](../docs/src/design.md#numeric-types-and-arithmetic)
+for every model and reduction. Before implementation, identify each numeric
+input and domain, each computed total and result type, the largest supported
+value, every range/sign-changing conversion, overflow behavior, and whether
+arithmetic is exact or approximate. Use `TryFrom` at range boundaries and
+checked arithmetic for derived values that may overflow. Rust construction,
+serde, CLI, and MCP must enforce the same range.
+
 ### File Naming
 - Reduction files: `src/rules/<source>_<target>.rs` (e.g., `maximumindependentset_qubo.rs`)
 - Model files: `src/models/<category>/<name>.rs` — category is by input structure: `graph/` (graph input), `formula/` (boolean formula/circuit), `set/` (universe + subsets), `algebraic/` (matrix/linear system/lattice), `misc/` (other)
diff --git a/.claude/skills/add-model/SKILL.md b/.claude/skills/add-model/SKILL.md
index 54f4c2292..903be1de1 100644
--- a/.claude/skills/add-model/SKILL.md
+++ b/.claude/skills/add-model/SKILL.md
@@ -27,6 +27,7 @@ Before any implementation, collect all required information. If called from `iss
 | 10 | **Solving strategy** | How it can be solved | "BruteForce works; ILP reduction available" |
 | 11 | **Category** | Which sub-module under `src/models/` | `graph`, `formula`, `set`, `algebraic`, `misc` |
 | 12 | **Expected outcome from the issue** | Concrete outcome for the issue's example instance | Objective: one optimal solution + optimal value. Witness: one valid/satisfying solution + why it is valid. Aggregate-only: the final aggregate value and how it is derived |
+| 13 | **Numeric contract** | Every numeric input/domain, computed total type, maximum supported value, checked conversion, overflow behavior, and exact/approximate choice | `weight: i32`, `total: i64`, exact, constructor rejects out-of-range input |
 
 If any item is missing, ask the user to provide it. Do NOT proceed until the checklist is complete.
 
@@ -75,6 +76,7 @@ Read these first to understand the patterns:
 ## Pre-review Checklist
 
 Before implementing, make sure the plan explicitly covers these items that structural review checks later:
+- Numeric choices follow `docs/src/design.md#numeric-types-and-arithmetic`; serde/CLI construction uses the same validation as `new`/`try_new`, and boundary tests cover the declared maximum without requiring impractical allocation
 - `ProblemSchemaEntry` metadata is complete for the current schema shape (`display_name`, `aliases`, `dimensions`, and constructor-facing `fields`)
 - `Problem::Value` uses the correct aggregate wrapper and witness support is intentional
 - `declare_variants!` is present with exactly one `default` variant when multiple concrete variants exist
diff --git a/.claude/skills/add-rule/SKILL.md b/.claude/skills/add-rule/SKILL.md
index 5e9b01ea6..9264a508a 100644
--- a/.claude/skills/add-rule/SKILL.md
+++ b/.claude/skills/add-rule/SKILL.md
@@ -33,6 +33,7 @@ Before any implementation, collect all required information. If called from `iss
 | 7 | **Concrete example** | A small worked-out instance (tutorial style, clear intuition) | "Triangle graph: VC={0,1} -> IS={2}" |
 | 8 | **Solving strategy** | How to solve the target problem | "BruteForce, or existing ILP reduction" |
 | 9 | **Reference** | Paper, textbook, or URL for the reduction | URL or citation |
+| 10 | **Numeric contract** | Source/target numeric fields, totals, size arithmetic, coefficients, bounds, auxiliary IDs, maximum values, checked conversions, overflow behavior, and exact/approximate choice | `usize` source count to checked `i32` SAT IDs |
 
 If any item is missing, ask the user to provide it. Put a high standard on item 7 (concrete example): it must be in tutorial style with clear intuition and easy to understand. Do NOT proceed until the checklist is complete.
 
@@ -56,6 +57,14 @@ grep "type Value = " src/models/*/<source_file>.rs src/models/*/<target_file>.rs
 
 If incompatible, STOP and comment on the issue explaining the type mismatch and options. Do NOT proceed.
 
+## Numeric Safety Gate
+
+Read `docs/src/design.md#numeric-types-and-arithmetic`. Reject an incomplete
+plan when numeric domains, total types, maxima, or conversions are unspecified.
+Do not use `as` for range/sign changes. Check target-size arithmetic and
+auxiliary identifiers before constructing the target, verify serde/CLI uses the
+same ranges, and add focused tests at the declared boundary.
+
 ## Reference Implementations
 
 Read these first to understand the patterns:
diff --git a/.claude/skills/review-structural/SKILL.md b/.claude/skills/review-structural/SKILL.md
index cdf144284..d32c6b3fb 100644
--- a/.claude/skills/review-structural/SKILL.md
+++ b/.claude/skills/review-structural/SKILL.md
@@ -66,6 +66,7 @@ Only run if review type includes "model". Given: problem name `P`, category `C`,
 | 14 | Canonical model example registered | `Grep("{P}", "src/example_db/model_builders.rs")` |
 | 15 | Paper `display-name` entry | `Grep('"{P}"', "docs/paper/reductions.typ")` |
 | 16 | Paper `problem-def` block | `Grep('problem-def.*"{P}"', "docs/paper/reductions.typ")` |
+| 17 | Numeric contract | Compare issue fields, schema types, Rust fields, aggregate/total type, constructor and serde validation, conversions, overflow behavior, and boundary tests against `docs/src/design.md#numeric-types-and-arithmetic` |
 
 ### Rule Checklist
 
@@ -85,6 +86,7 @@ Only run if review type includes "rule". Given: source `S`, target `T`, rule fil
 | 10 | Example-db lookup tests exist | `Grep("find_rule_example|build_rule_db", "src/unit_tests/example_db.rs")` |
 | 11 | Paper `reduction-rule` entry | `Grep('reduction-rule.*"{S}".*"{T}"', "docs/paper/reductions.typ")` |
 | 12 | Extraction contract | Direct decoders call `validate_target_solution()`, enforce rule-specific structure, and test malformed cases; the helper does not establish feasibility or optimality. Composed extractors may delegate. |
+| 13 | Numeric contract | Compare source/target types, size arithmetic, coefficients, bounds, auxiliary IDs, conversions, overflow behavior, and boundary tests against `docs/src/design.md#numeric-types-and-arithmetic` |
 
 ## Step 2b: Blacklisted File Check
 
@@ -111,12 +113,14 @@ Report pass/fail. If tests fail, identify which tests. **Do NOT fix anything** 
 2. **`dims()` correctness** — Does it return the actual configuration space? (e.g., `vec![2; n]` for binary)
 3. **Size getter consistency** — Do inherent getter methods (e.g., `num_vertices()`, `num_edges()`) match names used in overhead expressions?
 4. **Weight handling** — Are weights managed via inherent methods, not traits?
+5. **Numeric safety** — Are element and total types distinct where required, do serde and constructors enforce the same range, and are overflow and non-finite values rejected explicitly?
 
 ### For Rules:
 1. **`extract_solution` correctness** — Does it implement the mathematical inverse? Is every branch either a defined mathematical case or an `ExtractionError`, with no defaulting, truncation, clamping, panic, or recovery?
 2. **Overhead accuracy** — Does `overhead = { field = "expr" }` reflect the actual size relationship?
 3. **Example quality** — Is it tutorial-style? Does the JSON export include both source and target data?
 4. **Paper quality** — Is the reduction-rule statement precise? Is the proof sketch sound?
+5. **Numeric safety** — Are target sizes and auxiliary IDs checked before construction, with no unchecked narrowing or exact-to-`f64` shortcut?
 
 ## Step 5: Issue Compliance Review
 
diff --git a/.github/ISSUE_TEMPLATE/problem.md b/.github/ISSUE_TEMPLATE/problem.md
index 412397888..e5214d071 100644
--- a/.github/ISSUE_TEMPLATE/problem.md
+++ b/.github/ISSUE_TEMPLATE/problem.md
@@ -50,6 +50,18 @@ Connect fields to the symbols defined above.
 | <!-- e.g. graph --> | <!-- e.g. SimpleGraph --> | <!-- e.g. the graph G=(V,E) --> |
 | <!-- e.g. weights --> | <!-- e.g. list of W --> | <!-- e.g. vertex weights w_i for each i ∈ V (weighted variant only) --> |
 
+## Numeric Contract
+
+<!-- Follow docs/src/design.md#numeric-types-and-arithmetic. Distinguish the
+type of one input value from the type of a sum or product. -->
+
+| Quantity | Meaning and domain | Input type | Computed/total type | Maximum supported value | Checked conversions |
+|----------|--------------------|------------|---------------------|-------------------------|---------------------|
+| <!-- e.g. w_i --> | <!-- signed vertex weight --> | <!-- i32 --> | <!-- i64 total --> | <!-- i64::MAX total --> | <!-- i32 -> i64 via From --> |
+
+- **Overflow behavior:** <!-- What construction rejects and what error is reported -->
+- **Arithmetic:** <!-- Exact integer, or approximate f64 with justification -->
+
 ## Complexity
 
 - **Best known exact algorithm:** <!-- e.g. O(1.1996^n) by Xiao & Nagamochi (2017), where n = |V| -->
diff --git a/.github/ISSUE_TEMPLATE/rule.md b/.github/ISSUE_TEMPLATE/rule.md
index 230db8452..ca49e2dd2 100644
--- a/.github/ISSUE_TEMPLATE/rule.md
+++ b/.github/ISSUE_TEMPLATE/rule.md
@@ -45,6 +45,18 @@ Use the symbols defined in the Reduction Algorithm above. -->
 | <!-- e.g. number of variables --> | <!-- e.g. n = |V| --> |
 | <!-- e.g. number of edges --> | <!-- e.g. m = |E| --> |
 
+## Numeric Contract
+
+<!-- Follow docs/src/design.md#numeric-types-and-arithmetic. Include source and
+target values, size calculations, coefficients, bounds, and auxiliary IDs. -->
+
+| Quantity | Meaning and domain | Source type | Target/computed type | Maximum supported value | Checked conversions |
+|----------|--------------------|-------------|----------------------|-------------------------|---------------------|
+| <!-- e.g. auxiliary variable --> | <!-- positive SAT variable ID --> | <!-- usize count --> | <!-- i32 literal --> | <!-- i32::MAX --> | <!-- i32::try_from --> |
+
+- **Overflow behavior:** <!-- Where the reduction stops and what error is reported -->
+- **Arithmetic:** <!-- Exact integer, or approximate f64 with justification -->
+
 ## Validation Method
 
 <!-- How to verify the reduction is correct beyond closed-loop testing?
diff --git a/docs/src/design.md b/docs/src/design.md
index 20f351018..fcbbf90b3 100644
--- a/docs/src/design.md
+++ b/docs/src/design.md
@@ -2,6 +2,9 @@
 
 This guide covers the library internals for contributors.
 
+See [Numeric types and arithmetic](#numeric-types-and-arithmetic) before
+choosing numeric fields or implementing arithmetic in a model or reduction.
+
 ## Module Architecture
 
 <script src="https://unpkg.com/cytoscape@3.30.4/dist/cytoscape.min.js"></script>
@@ -45,6 +48,93 @@ trait Problem: Clone {
 - **Aggregate-only problems** — use fold values such as `Sum<W>` or `And`; these solve to a value but do not admit representative witness configurations.
 - **Common aggregate wrappers** — `Max<V>`, `Min<V>`, `Sum<W>`, `Or`, `And`, `Extremum<V>`, `ExtremumSense`.
 
+## Numeric types and arithmetic
+
+Every numeric field needs a mathematical domain, a supported range, and an
+overflow rule. `NumericSize` only lists operations required by aggregate value
+types; it does not make those operations overflow-safe.
+
+| Quantity | Normal Rust type | Supported range and rule | Repository example |
+|---|---|---|---|
+| Collection index, length, or in-memory configuration dimension | `usize` | Values supported by the current target. Convert external fixed-width values with `usize::try_from`; reject values that do not fit. | `Problem::dims()` and graph vertex indices |
+| Individual exact signed weight or cost | `i32` | The `i32` range, narrowed further when the problem requires nonnegative input. | A vertex weight in `MinimumDominatingSet<_, i32>` |
+| Total of `i32` weights | `i64` | Accumulate exactly in `i64`; reject a derived value that would exceed `i64`. | `WeightElement for i32` uses `Sum = i64` |
+| Unit-weight count | `i64` | Use the same total and bound representation as exact weighted variants. | `WeightElement for One` uses `Sum = i64` |
+| Approximate numeric input | `f64` | Only when approximation belongs to the model or solver interface; model constructors reject NaN and infinity. | Floating-point QUBO coefficients |
+| Fixed-width serialized nonnegative domain value | `u64` | The same JSON range on every target. Convert to `usize` before indexing and reject failure. | Large integer sizes in arithmetic problems |
+| Exact signed objective bound | The objective total type, normally `i64` | A decision bound and the optimization result it compares against use the same type. | `Decision<MinimumVertexCover<_, i32>>` has an `i64` bound |
+| SAT variable count | `usize`, at most `i32::MAX` | Reject larger formulas at construction because signed literals cannot encode them. | `Satisfiability::try_new` |
+| SAT literal | nonzero `i32` | Its magnitude must be in `1..=num_vars`; `0` and `i32::MIN` are invalid. | `CNFClause` literals |
+
+### Indices and collection sizes
+
+Use `usize` for values passed to indexing, collection allocation, and
+configuration dimensions. A serialized `usize` is intentionally machine-sized:
+loading rejects a JSON value that does not fit the target. Use `u64` instead
+when the problem definition requires a fixed serialized range, then perform an
+explicit checked conversion before using it as an index.
+
+### Weights, costs, times, capacities, and bounds
+
+Choose an input type from the mathematical domain, not from the type of a later
+index. Exact signed element weights normally use `i32`. A quantity that bounds
+or compares with a total uses the total's type. Negative values are accepted
+only when the problem definition gives them meaning; otherwise reject them in
+the constructor.
+
+### Totals and derived arithmetic
+
+Do not assume one input element's type can hold a sum or product of many
+elements. `WeightElement` is the source of truth for weight totals: `i32` and
+`One` accumulate into `i64`, while `f64` accumulates into `f64`. For other
+derived integers, choose a result type from the largest supported value and use
+`checked_add`, `checked_sub`, or `checked_mul` when the operation may reach its
+boundary. Overflow is an input/construction error, not an infeasible solution.
+
+### Conversions
+
+Use `From` for conversions that cannot change the value and `TryFrom` when
+range or sign can change. Do not use `as` for a user/model-derived narrowing,
+signedness change, SAT variable number, coefficient, or bound. A failed
+conversion must report the value, destination range, and model or reduction
+that rejected it.
+
+### JSON, CLI, and MCP boundaries
+
+The schema field type is the external contract. Rust constructors and serde
+deserialization must apply the same validation, and schema-driven CLI/MCP
+creation must parse the declared type rather than a smaller intermediate type.
+Do not deserialize directly into private validated fields when doing so bypasses
+the constructor invariant.
+
+### SAT and compact signed encodings
+
+CNF uses one-indexed signed `i32` literals. All CNF-backed models validate the
+same range during construction and deserialization. Reductions that create
+auxiliary SAT variables allocate them through the checked SAT allocator; they
+must stop before constructing a target if the next ID would exceed
+`i32::MAX`. Apply the same explicit-range rule to any new compact signed
+encoding.
+
+### Exact integers and floating point
+
+Keep exact integer calculations in integer types. Do not convert an exact sum,
+product, identifier, or comparison bound to `f64` merely to obtain more range.
+An integer-to-floating conversion is permitted only at an explicitly
+approximate solver boundary, where the exactly representable input range and
+out-of-range behavior are documented.
+
+### Numeric review checklist
+
+For every new model or reduction, record:
+
+1. every numeric input, its meaning, and its mathematical domain;
+2. every computed total/product and its result type;
+3. the largest supported input and derived value;
+4. every narrowing or signedness-changing conversion;
+5. how construction, deserialization, and reduction report overflow;
+6. whether arithmetic is exact or approximate, with justification for `f64`.
+
 ## Variant System
 
 A single problem name like `MaximumIndependentSet` can have multiple **variants** — carrying weights on vertices, or defined on a restricted topology (e.g., king's subgraph). Variants form a subtype hierarchy: independent sets on king's subgraphs are a subset of independent sets on unit-disk graphs. The reduction from a more specific variant to a less specific one is a **variant cast** — an identity mapping where indices are preserved.
diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs
index 588eb7fda..81ac482a1 100644
--- a/problemreductions-cli/src/commands/create.rs
+++ b/problemreductions-cli/src/commands/create.rs
@@ -693,7 +693,7 @@ fn ser_decision_minimum_vertex_cover_with<
 >(
     graph: G,
     weights: Vec<i32>,
-    bound: i32,
+    bound: i64,
 ) -> Result<serde_json::Value> {
     ser(Decision::new(
         MinimumVertexCover::new(graph, weights),
@@ -1827,11 +1827,7 @@ fn create_random(
                 raw_bound >= 0,
                 "DecisionMinimumVertexCover: --bound must be non-negative"
             );
-            let bound = i32::try_from(raw_bound).map_err(|_| {
-                anyhow::anyhow!(
-                    "DecisionMinimumVertexCover: --bound must fit in a 32-bit signed integer, got {raw_bound}"
-                )
-            })?;
+            let bound = raw_bound;
             let weights = vec![1i32; num_vertices];
             match graph_type {
                 "KingsSubgraph" => {
diff --git a/problemreductions-cli/src/commands/create/schema_support.rs b/problemreductions-cli/src/commands/create/schema_support.rs
index d7ecb3497..51010b637 100644
--- a/problemreductions-cli/src/commands/create/schema_support.rs
+++ b/problemreductions-cli/src/commands/create/schema_support.rs
@@ -456,7 +456,7 @@ pub(super) fn resolve_schema_field_type(
 
 pub(super) fn weight_sum_type(weight_type: &str) -> &'static str {
     match weight_type {
-        "One" | "i32" => "i32",
+        "One" | "i32" => "i64",
         "f64" => "f64",
         _ => "i32",
     }
diff --git a/src/models/formula/ksat.rs b/src/models/formula/ksat.rs
index 1dc118638..e53d094de 100644
--- a/src/models/formula/ksat.rs
+++ b/src/models/formula/ksat.rs
@@ -8,9 +8,9 @@
 use crate::registry::{FieldInfo, ProblemSchemaEntry, VariantDimension};
 use crate::traits::Problem;
 use crate::variant::{KValue, K2, K3, KN};
-use serde::{Deserialize, Serialize};
+use serde::{de::Error as _, Deserialize, Deserializer, Serialize};
 
-use super::CNFClause;
+use super::{sat::validate_cnf_literals, CNFClause};
 
 pub(crate) fn first_n_odd_primes(count: usize) -> Vec<u64> {
     let mut primes = Vec::with_capacity(count);
@@ -93,8 +93,7 @@ inventory::submit! {
 /// let solutions = solver.find_all_witnesses(&problem);
 /// assert!(!solutions.is_empty());
 /// ```
-#[derive(Debug, Clone, Serialize, Deserialize)]
-#[serde(bound(deserialize = ""))]
+#[derive(Debug, Clone, Serialize)]
 pub struct KSatisfiability<K: KValue> {
     /// Number of variables.
     num_vars: usize,
@@ -104,6 +103,22 @@ pub struct KSatisfiability<K: KValue> {
     _phantom: std::marker::PhantomData<K>,
 }
 
+#[derive(Deserialize)]
+struct KSatisfiabilityDef {
+    num_vars: usize,
+    clauses: Vec<CNFClause>,
+}
+
+impl<'de, K: KValue> Deserialize<'de> for KSatisfiability<K> {
+    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
+    where
+        D: Deserializer<'de>,
+    {
+        let value = KSatisfiabilityDef::deserialize(deserializer)?;
+        Self::try_new(value.num_vars, value.clauses).map_err(D::Error::custom)
+    }
+}
+
 impl<K: KValue> KSatisfiability<K> {
     /// Create a new K-SAT problem.
     ///
@@ -112,22 +127,27 @@ impl<K: KValue> KSatisfiability<K> {
     /// concrete value like K2, K3). When K is KN (arbitrary), no clause-length
     /// validation is performed.
     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.
+    pub fn try_new(num_vars: usize, clauses: Vec<CNFClause>) -> Result<Self, String> {
+        validate_cnf_literals(num_vars, &clauses)?;
         if let Some(k) = K::K {
             for (i, clause) in clauses.iter().enumerate() {
-                assert!(
-                    clause.len() == k,
-                    "Clause {} has {} literals, expected {}",
-                    i,
-                    clause.len(),
-                    k
-                );
+                if clause.len() != k {
+                    return Err(format!(
+                        "Clause {i} has {} literals, expected {k}",
+                        clause.len()
+                    ));
+                }
             }
         }
-        Self {
+        Ok(Self {
             num_vars,
             clauses,
             _phantom: std::marker::PhantomData,
-        }
+        })
     }
 
     /// Create a new K-SAT problem allowing clauses with fewer than K literals.
@@ -140,22 +160,27 @@ impl<K: KValue> KSatisfiability<K> {
     /// 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, String> {
+        validate_cnf_literals(num_vars, &clauses)?;
         if let Some(k) = K::K {
             for (i, clause) in clauses.iter().enumerate() {
-                assert!(
-                    clause.len() <= k,
-                    "Clause {} has {} literals, expected at most {}",
-                    i,
-                    clause.len(),
-                    k
-                );
+                if clause.len() > k {
+                    return Err(format!(
+                        "Clause {i} has {} literals, expected at most {k}",
+                        clause.len()
+                    ));
+                }
             }
         }
-        Self {
+        Ok(Self {
             num_vars,
             clauses,
             _phantom: std::marker::PhantomData,
-        }
+        })
     }
 
     /// Get the number of variables.
diff --git a/src/models/formula/maximum_2_satisfiability.rs b/src/models/formula/maximum_2_satisfiability.rs
index 6d9f20843..ee6f83fd8 100644
--- a/src/models/formula/maximum_2_satisfiability.rs
+++ b/src/models/formula/maximum_2_satisfiability.rs
@@ -9,7 +9,7 @@ use crate::traits::Problem;
 use crate::types::Max;
 use serde::{Deserialize, Serialize};
 
-use super::CNFClause;
+use super::{sat::validate_cnf_literals, CNFClause};
 
 inventory::submit! {
     ProblemSchemaEntry {
@@ -51,6 +51,7 @@ inventory::submit! {
 /// let value = solver.solve(&problem);
 /// ```
 #[derive(Debug, Clone, Serialize, Deserialize)]
+#[serde(try_from = "Maximum2SatisfiabilityDef")]
 pub struct Maximum2Satisfiability {
     /// Number of Boolean variables.
     num_vars: usize,
@@ -64,15 +65,21 @@ impl Maximum2Satisfiability {
     /// # Panics
     /// Panics if any clause does not have exactly 2 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 new MAX-2-SAT problem after validating its clauses.
+    pub fn try_new(num_vars: usize, clauses: Vec<CNFClause>) -> Result<Self, String> {
+        validate_cnf_literals(num_vars, &clauses)?;
         for (i, clause) in clauses.iter().enumerate() {
-            assert!(
-                clause.len() == 2,
-                "Clause {} has {} literals, expected 2",
-                i,
-                clause.len()
-            );
+            if clause.len() != 2 {
+                return Err(format!(
+                    "Clause {i} has {} literals, expected 2",
+                    clause.len()
+                ));
+            }
         }
-        Self { num_vars, clauses }
+        Ok(Self { num_vars, clauses })
     }
 
     /// Get the number of variables.
@@ -121,6 +128,20 @@ crate::declare_variants! {
     default Maximum2Satisfiability => "2^(0.7905 * num_variables)",
 }
 
+#[derive(Deserialize)]
+struct Maximum2SatisfiabilityDef {
+    num_vars: usize,
+    clauses: Vec<CNFClause>,
+}
+
+impl TryFrom<Maximum2SatisfiabilityDef> for Maximum2Satisfiability {
+    type Error = String;
+
+    fn try_from(value: Maximum2SatisfiabilityDef) -> Result<Self, Self::Error> {
+        Self::try_new(value.num_vars, value.clauses)
+    }
+}
+
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
     vec![crate::example_db::specs::ModelExampleSpec {
diff --git a/src/models/formula/mod.rs b/src/models/formula/mod.rs
index e2c09d8d8..6b4fe0725 100644
--- a/src/models/formula/mod.rs
+++ b/src/models/formula/mod.rs
@@ -29,6 +29,7 @@ pub use non_tautology::NonTautology;
 pub use one_in_three_satisfiability::OneInThreeSatisfiability;
 pub use planar_3_satisfiability::Planar3Satisfiability;
 pub use qbf::{QuantifiedBooleanFormulas, Quantifier};
+pub(crate) use sat::SatVariableAllocator;
 pub use sat::{CNFClause, Satisfiability};
 
 /// Convert a binary config (0/1 per variable) to a boolean assignment.
diff --git a/src/models/formula/nae_satisfiability.rs b/src/models/formula/nae_satisfiability.rs
index 5e79f2de4..834b9a4e7 100644
--- a/src/models/formula/nae_satisfiability.rs
+++ b/src/models/formula/nae_satisfiability.rs
@@ -7,7 +7,7 @@ use crate::registry::{FieldInfo, ProblemSchemaEntry};
 use crate::traits::Problem;
 use serde::{Deserialize, Serialize};
 
-use super::CNFClause;
+use super::{sat::validate_cnf_literals, CNFClause};
 
 inventory::submit! {
     ProblemSchemaEntry {
@@ -50,6 +50,7 @@ impl NAESatisfiability {
     /// Create a new NAE-SAT problem, returning an error instead of panicking
     /// when a clause has fewer than two literals.
     pub fn try_new(num_vars: usize, clauses: Vec<CNFClause>) -> Result<Self, String> {
+        validate_cnf_literals(num_vars, &clauses)?;
         validate_clause_lengths(&clauses)?;
         Ok(Self { num_vars, clauses })
     }
diff --git a/src/models/formula/one_in_three_satisfiability.rs b/src/models/formula/one_in_three_satisfiability.rs
index 8b5453ee3..6a6c87597 100644
--- a/src/models/formula/one_in_three_satisfiability.rs
+++ b/src/models/formula/one_in_three_satisfiability.rs
@@ -8,7 +8,7 @@ use crate::registry::{FieldInfo, ProblemSchemaEntry};
 use crate::traits::Problem;
 use serde::{Deserialize, Serialize};
 
-use super::CNFClause;
+use super::{sat::validate_cnf_literals, CNFClause};
 
 inventory::submit! {
     ProblemSchemaEntry {
@@ -55,6 +55,7 @@ inventory::submit! {
 /// assert!(solution.is_some());
 /// ```
 #[derive(Debug, Clone, Serialize, Deserialize)]
+#[serde(try_from = "OneInThreeSatisfiabilityDef")]
 pub struct OneInThreeSatisfiability {
     /// Number of variables.
     num_vars: usize,
@@ -69,26 +70,21 @@ impl OneInThreeSatisfiability {
     /// Panics if any clause does not have exactly 3 literals, or if any
     /// literal references a variable outside the range [1, num_vars].
     pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
+        Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
+    }
+
+    /// Create a new 1-in-3 SAT problem after validating its clauses.
+    pub fn try_new(num_vars: usize, clauses: Vec<CNFClause>) -> Result<Self, String> {
+        validate_cnf_literals(num_vars, &clauses)?;
         for (i, clause) in clauses.iter().enumerate() {
-            assert!(
-                clause.len() == 3,
-                "Clause {} has {} literals, expected 3",
-                i,
-                clause.len()
-            );
-            for &lit in &clause.literals {
-                let var = lit.unsigned_abs() as usize;
-                assert!(
-                    var >= 1 && var <= num_vars,
-                    "Clause {} contains literal {} referencing variable {} outside range [1, {}]",
-                    i,
-                    lit,
-                    var,
-                    num_vars
-                );
+            if clause.len() != 3 {
+                return Err(format!(
+                    "Clause {i} has {} literals, expected 3",
+                    clause.len()
+                ));
             }
         }
-        Self { num_vars, clauses }
+        Ok(Self { num_vars, clauses })
     }
 
     /// Get the number of variables.
@@ -156,6 +152,20 @@ crate::declare_variants! {
     default OneInThreeSatisfiability => "1.307^num_variables",
 }
 
+#[derive(Deserialize)]
+struct OneInThreeSatisfiabilityDef {
+    num_vars: usize,
+    clauses: Vec<CNFClause>,
+}
+
+impl TryFrom<OneInThreeSatisfiabilityDef> for OneInThreeSatisfiability {
+    type Error = String;
+
+    fn try_from(value: OneInThreeSatisfiabilityDef) -> Result<Self, Self::Error> {
+        Self::try_new(value.num_vars, value.clauses)
+    }
+}
+
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
     vec![crate::example_db::specs::ModelExampleSpec {
diff --git a/src/models/formula/planar_3_satisfiability.rs b/src/models/formula/planar_3_satisfiability.rs
index b3b91871b..6162c19bf 100644
--- a/src/models/formula/planar_3_satisfiability.rs
+++ b/src/models/formula/planar_3_satisfiability.rs
@@ -9,7 +9,7 @@ use crate::registry::{FieldInfo, ProblemSchemaEntry};
 use crate::traits::Problem;
 use serde::{Deserialize, Serialize};
 
-use super::CNFClause;
+use super::{sat::validate_cnf_literals, CNFClause};
 
 inventory::submit! {
     ProblemSchemaEntry {
@@ -64,6 +64,7 @@ inventory::submit! {
 /// assert!(solution.is_some());
 /// ```
 #[derive(Debug, Clone, Serialize, Deserialize)]
+#[serde(try_from = "Planar3SatisfiabilityDef")]
 pub struct Planar3Satisfiability {
     /// Number of variables.
     num_vars: usize,
@@ -80,26 +81,21 @@ impl Planar3Satisfiability {
     ///
     /// **Note:** Planarity of the incidence graph is not checked.
     pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
+        Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
+    }
+
+    /// Create a new Planar 3-SAT problem after validating its clauses.
+    pub fn try_new(num_vars: usize, clauses: Vec<CNFClause>) -> Result<Self, String> {
+        validate_cnf_literals(num_vars, &clauses)?;
         for (i, clause) in clauses.iter().enumerate() {
-            assert!(
-                clause.len() == 3,
-                "Clause {} has {} literals, expected 3",
-                i,
-                clause.len()
-            );
-            for &lit in &clause.literals {
-                let var = lit.unsigned_abs() as usize;
-                assert!(
-                    var >= 1 && var <= num_vars,
-                    "Clause {} contains literal {} referencing variable {} outside range [1, {}]",
-                    i,
-                    lit,
-                    var,
-                    num_vars
-                );
+            if clause.len() != 3 {
+                return Err(format!(
+                    "Clause {i} has {} literals, expected 3",
+                    clause.len()
+                ));
             }
         }
-        Self { num_vars, clauses }
+        Ok(Self { num_vars, clauses })
     }
 
     /// Get the number of variables.
@@ -152,6 +148,20 @@ crate::declare_variants! {
     default Planar3Satisfiability => "1.307^num_variables",
 }
 
+#[derive(Deserialize)]
+struct Planar3SatisfiabilityDef {
+    num_vars: usize,
+    clauses: Vec<CNFClause>,
+}
+
+impl TryFrom<Planar3SatisfiabilityDef> for Planar3Satisfiability {
+    type Error = String;
+
+    fn try_from(value: Planar3SatisfiabilityDef) -> Result<Self, Self::Error> {
+        Self::try_new(value.num_vars, value.clauses)
+    }
+}
+
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
     vec![crate::example_db::specs::ModelExampleSpec {
diff --git a/src/models/formula/qbf.rs b/src/models/formula/qbf.rs
index d202e9f17..c47b88bcc 100644
--- a/src/models/formula/qbf.rs
+++ b/src/models/formula/qbf.rs
@@ -8,7 +8,7 @@
 //! ∀ (ForAll) or ∃ (Exists) and E is a Boolean expression in CNF,
 //! determine whether F is true.
 
-use crate::models::formula::CNFClause;
+use crate::models::formula::{sat::validate_cnf_literals, CNFClause};
 use crate::registry::{FieldInfo, ProblemSchemaEntry};
 use crate::traits::Problem;
 use serde::{Deserialize, Serialize};
@@ -63,6 +63,7 @@ pub enum Quantifier {
 /// assert!(problem.is_true());
 /// ```
 #[derive(Debug, Clone, Serialize, Deserialize)]
+#[serde(try_from = "QuantifiedBooleanFormulasDef")]
 pub struct QuantifiedBooleanFormulas {
     /// Number of variables.
     num_vars: usize,
@@ -79,18 +80,27 @@ impl QuantifiedBooleanFormulas {
     ///
     /// Panics if `quantifiers.len() != num_vars`.
     pub fn new(num_vars: usize, quantifiers: Vec<Quantifier>, clauses: Vec<CNFClause>) -> Self {
-        assert_eq!(
-            quantifiers.len(),
-            num_vars,
-            "quantifiers length ({}) must equal num_vars ({})",
-            quantifiers.len(),
-            num_vars
-        );
-        Self {
+        Self::try_new(num_vars, quantifiers, clauses).unwrap_or_else(|message| panic!("{message}"))
+    }
+
+    /// Create a QBF problem after validating its quantifiers and CNF literals.
+    pub fn try_new(
+        num_vars: usize,
+        quantifiers: Vec<Quantifier>,
+        clauses: Vec<CNFClause>,
+    ) -> Result<Self, String> {
+        if quantifiers.len() != num_vars {
+            return Err(format!(
+                "quantifiers length ({}) must equal num_vars ({num_vars})",
+                quantifiers.len()
+            ));
+        }
+        validate_cnf_literals(num_vars, &clauses)?;
+        Ok(Self {
             num_vars,
             quantifiers,
             clauses,
-        }
+        })
     }
 
     /// Get the number of variables.
@@ -181,6 +191,21 @@ crate::declare_variants! {
     default QuantifiedBooleanFormulas => "2^num_vars",
 }
 
+#[derive(Deserialize)]
+struct QuantifiedBooleanFormulasDef {
+    num_vars: usize,
+    quantifiers: Vec<Quantifier>,
+    clauses: Vec<CNFClause>,
+}
+
+impl TryFrom<QuantifiedBooleanFormulasDef> for QuantifiedBooleanFormulas {
+    type Error = String;
+
+    fn try_from(value: QuantifiedBooleanFormulasDef) -> Result<Self, Self::Error> {
+        Self::try_new(value.num_vars, value.quantifiers, value.clauses)
+    }
+}
+
 #[cfg(feature = "example-db")]
 pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
     vec![crate::example_db::specs::ModelExampleSpec {
diff --git a/src/models/formula/sat.rs b/src/models/formula/sat.rs
index 8be2e2b90..0cc5a44ca 100644
--- a/src/models/formula/sat.rs
+++ b/src/models/formula/sat.rs
@@ -54,7 +54,10 @@ impl CNFClause {
     /// * `assignment` - Boolean assignment, 0-indexed
     pub fn is_satisfied(&self, assignment: &[bool]) -> bool {
         self.literals.iter().any(|&lit| {
-            let var = lit.unsigned_abs() as usize - 1; // Convert to 0-indexed
+            let var = usize::try_from(lit.unsigned_abs())
+                .expect("u32 literal magnitude must fit usize")
+                .checked_sub(1)
+                .expect("CNF literal 0 is invalid");
             let value = assignment.get(var).copied().unwrap_or(false);
             if lit > 0 {
                 value
@@ -68,7 +71,12 @@ impl CNFClause {
     pub fn variables(&self) -> Vec<usize> {
         self.literals
             .iter()
-            .map(|&lit| lit.unsigned_abs() as usize - 1)
+            .map(|&lit| {
+                usize::try_from(lit.unsigned_abs())
+                    .expect("u32 literal magnitude must fit usize")
+                    .checked_sub(1)
+                    .expect("CNF literal 0 is invalid")
+            })
             .collect()
     }
 
@@ -114,6 +122,7 @@ impl CNFClause {
 /// }
 /// ```
 #[derive(Debug, Clone, Serialize, Deserialize)]
+#[serde(try_from = "SatisfiabilityDef")]
 pub struct Satisfiability {
     /// Number of variables.
     num_vars: usize,
@@ -124,7 +133,13 @@ pub struct Satisfiability {
 impl Satisfiability {
     /// Create a new SAT problem.
     pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self {
-        Self { num_vars, clauses }
+        Self::try_new(num_vars, clauses).unwrap_or_else(|message| panic!("{message}"))
+    }
+
+    /// Create a new SAT problem after validating its literal encoding.
+    pub fn try_new(num_vars: usize, clauses: Vec<CNFClause>) -> Result<Self, String> {
+        validate_cnf_literals(num_vars, &clauses)?;
+        Ok(Self { num_vars, clauses })
     }
 
     /// Get the number of variables.
@@ -197,6 +212,112 @@ crate::declare_variants! {
     default Satisfiability => "2^num_variables",
 }
 
+#[derive(Deserialize)]
+struct SatisfiabilityDef {
+    num_vars: usize,
+    clauses: Vec<CNFClause>,
+}
+
+impl TryFrom<SatisfiabilityDef> for Satisfiability {
+    type Error = String;
+
+    fn try_from(value: SatisfiabilityDef) -> Result<Self, Self::Error> {
+        Self::try_new(value.num_vars, value.clauses)
+    }
+}
+
+pub(super) fn validate_cnf_literals(num_vars: usize, clauses: &[CNFClause]) -> Result<(), String> {
+    if num_vars > i32::MAX as usize {
+        return Err(format!(
+            "num_vars {num_vars} exceeds the SAT literal limit {}",
+            i32::MAX
+        ));
+    }
+
+    for (clause_index, clause) in clauses.iter().enumerate() {
+        for &literal in &clause.literals {
+            if literal == 0 || literal == i32::MIN {
+                return Err(format!(
+                    "clause {clause_index} contains invalid literal {literal}; allowed variable numbers are 1..={num_vars} with either sign"
+                ));
+            }
+            if usize::try_from(literal.unsigned_abs())
+                .expect("SAT literal magnitude must fit usize")
+                > num_vars
+            {
+                return Err(format!(
+                    "clause {clause_index} contains invalid literal {literal}; allowed variable numbers are 1..={num_vars} with either sign"
+                ));
+            }
+        }
+    }
+
+    Ok(())
+}
+
+#[derive(Debug)]
+pub(crate) struct SatVariableAllocator {
+    reduction: &'static str,
+    next: u64,
+}
+
+impl SatVariableAllocator {
+    pub(crate) fn new(reduction: &'static str, existing: usize) -> Result<Self, String> {
+        if existing > i32::MAX as usize {
+            return Err(format!(
+                "{reduction} has {existing} source variables; SAT variable numbers are limited to {}",
+                i32::MAX
+            ));
+        }
+        Ok(Self {
+            reduction,
+            next: u64::try_from(existing).expect("usize SAT count fits u64") + 1,
+        })
+    }
+
+    pub(crate) fn allocate(&mut self) -> Result<i32, String> {
+        let variable = self.next;
+        if variable > i32::MAX as u64 {
+            return Err(format!(
+                "{} cannot allocate 1 auxiliary variable after {}; SAT variable numbers are limited to {}",
+                self.reduction,
+                self.num_vars(),
+                i32::MAX
+            ));
+        }
+        self.next += 1;
+        Ok(i32::try_from(variable).expect("checked SAT variable fits i32"))
+    }
+
+    pub(crate) fn allocate_many(&mut self, count: usize) -> Result<Vec<i32>, String> {
+        if count == 0 {
+            return Ok(Vec::new());
+        }
+        let count = u64::try_from(count).expect("usize allocation count fits u64");
+        let last = self
+            .next
+            .checked_add(count - 1)
+            .ok_or_else(|| format!("{} auxiliary variable count overflow", self.reduction))?;
+        if last > i32::MAX as u64 {
+            return Err(format!(
+                "{} cannot allocate {count} auxiliary variables after {}; SAT variable numbers are limited to {}",
+                self.reduction,
+                self.num_vars(),
+                i32::MAX
+            ));
+        }
+        let variables = (self.next..=last)
+            .map(|variable| i32::try_from(variable).expect("checked SAT variable fits i32"))
+            .collect();
+        self.next = last + 1;
+        Ok(variables)
+    }
+
+    pub(crate) fn num_vars(&self) -> usize {
+        usize::try_from(self.next - 1).expect("SAT variable count fits usize")
+    }
+}
+
 /// Check if an assignment satisfies a SAT formula.
 ///
 /// # Arguments
diff --git a/src/models/graph/mixed_chinese_postman.rs b/src/models/graph/mixed_chinese_postman.rs
index 866e2ecb7..af333f700 100644
--- a/src/models/graph/mixed_chinese_postman.rs
+++ b/src/models/graph/mixed_chinese_postman.rs
@@ -39,13 +39,13 @@ inventory::submit! {
 /// Postman subproblem, using all available arcs (including both directions of
 /// every undirected edge) for degree-balancing detours.
 #[derive(Debug, Clone, Serialize, Deserialize)]
-pub struct MixedChinesePostman<W: WeightElement<Sum = i32>> {
+pub struct MixedChinesePostman<W: WeightElement<Sum = i64>> {
     graph: MixedGraph,
     arc_weights: Vec<W>,
     edge_weights: Vec<W>,
 }
 
-impl<W: WeightElement<Sum = i32>> MixedChinesePostman<W> {
+impl<W: WeightElement<Sum = i64>> MixedChinesePostman<W> {
     /// Create a new mixed Chinese postman instance.
     ///
     /// # Panics
@@ -157,11 +157,11 @@ impl<W: WeightElement<Sum = i32>> MixedChinesePostman<W> {
             .arcs()
             .into_iter()
             .zip(self.arc_weights.iter())
-            .map(|((u, v), weight)| (u, v, i64::from(weight.to_sum())))
+            .map(|((u, v), weight)| (u, v, weight.to_sum()))
             .collect();
 
         for ((u, v), weight) in self.graph.edges().iter().zip(self.edge_weights.iter()) {
-            let cost = i64::from(weight.to_sum());
+            let cost = weight.to_sum();
             arcs.push((*u, *v, cost));
             arcs.push((*v, *u, cost));
         }
@@ -172,19 +172,19 @@ impl<W: WeightElement<Sum = i32>> MixedChinesePostman<W> {
     fn base_cost(&self) -> i64 {
         self.arc_weights
             .iter()
-            .map(|weight| i64::from(weight.to_sum()))
+            .map(WeightElement::to_sum)
             .sum::<i64>()
             + self
                 .edge_weights
                 .iter()
-                .map(|weight| i64::from(weight.to_sum()))
+                .map(WeightElement::to_sum)
                 .sum::<i64>()
     }
 }
 
 impl<W> MixedChinesePostman<W>
 where
-    W: WeightElement<Sum = i32> + crate::variant::VariantParam,
+    W: WeightElement<Sum = i64> + crate::variant::VariantParam,
 {
     /// Check whether a configuration yields a valid orientation (strongly
     /// connected with proper coverage).
@@ -195,7 +195,7 @@ where
 
 impl<W> Problem for MixedChinesePostman<W>
 where
-    W: WeightElement<Sum = i32> + crate::variant::VariantParam,
+    W: WeightElement<Sum = i64> + crate::variant::VariantParam,
 {
     const NAME: &'static str = "MixedChinesePostman";
     type Value = Min<W::Sum>;
@@ -233,7 +233,7 @@ where
         };
 
         let total = self.base_cost() + extra_cost;
-        Min(Some(total as W::Sum))
+        Min(Some(total))
     }
 }
 
diff --git a/src/rules/circuit_sat.rs b/src/rules/circuit_sat.rs
index 384ba8770..4f9549caa 100644
--- a/src/rules/circuit_sat.rs
+++ b/src/rules/circuit_sat.rs
@@ -1,7 +1,7 @@
 //! Reduction from CircuitSAT to Satisfiability via Tseitin encoding.
 
 use crate::models::formula::{
-    Assignment, BooleanExpr, BooleanOp, CNFClause, CircuitSAT, Satisfiability,
+    Assignment, BooleanExpr, BooleanOp, CNFClause, CircuitSAT, SatVariableAllocator, Satisfiability,
 };
 use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
@@ -33,21 +33,26 @@ struct TseitinEncoding {
 struct TseitinEncoder {
     source_var_ids: HashMap<String, i32>,
     clauses: Vec<CNFClause>,
-    next_var: i32,
+    variables: SatVariableAllocator,
 }
 
 impl TseitinEncoder {
     fn new(source: &CircuitSAT) -> Self {
+        let mut variables = SatVariableAllocator::new("CircuitSAT -> Satisfiability", 0)
+            .unwrap_or_else(|message| panic!("{message}"));
+        let source_ids = variables
+            .allocate_many(source.num_variables())
+            .unwrap_or_else(|message| panic!("{message}"));
         let source_var_ids = source
             .variable_names()
             .iter()
-            .enumerate()
-            .map(|(index, name)| (name.clone(), index as i32 + 1))
+            .zip(source_ids)
+            .map(|(name, variable)| (name.clone(), variable))
             .collect();
         Self {
             source_var_ids,
             clauses: Vec::new(),
-            next_var: source.num_variables() as i32 + 1,
+            variables,
         }
     }
 
@@ -57,7 +62,7 @@ impl TseitinEncoder {
         }
 
         TseitinEncoding {
-            num_vars: (self.next_var - 1) as usize,
+            num_vars: self.variables.num_vars(),
             clauses: self.clauses,
         }
     }
@@ -152,9 +157,9 @@ impl TseitinEncoder {
     }
 
     fn allocate_auxiliary_var(&mut self) -> i32 {
-        let var = self.next_var;
-        self.next_var += 1;
-        var
+        self.variables
+            .allocate()
+            .unwrap_or_else(|message| panic!("{message}"))
     }
 
     fn push_equivalence(&mut self, left: i32, right: i32) {
diff --git a/src/rules/exactcoverby3sets_boundeddiameterspanningtree.rs b/src/rules/exactcoverby3sets_boundeddiameterspanningtree.rs
index 882c3b958..61bd69d85 100644
--- a/src/rules/exactcoverby3sets_boundeddiameterspanningtree.rs
+++ b/src/rules/exactcoverby3sets_boundeddiameterspanningtree.rs
@@ -131,7 +131,12 @@ impl ReduceTo<BoundedDiameterSpanningTree<SimpleGraph, i32>> for ExactCoverBy3Se
             }
         }
 
-        let weight_bound: i32 = (4 * q + m + 2) as i32;
+        let weight_bound = q
+            .checked_mul(4)
+            .and_then(|value| value.checked_add(m))
+            .and_then(|value| value.checked_add(2))
+            .and_then(|value| i64::try_from(value).ok())
+            .expect("ExactCoverBy3Sets -> BoundedDiameterSpanningTree weight bound must fit i64");
         let diameter_bound: usize = 4;
 
         let graph = SimpleGraph::new(num_vertices, edges);
diff --git a/src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs b/src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs
index 5b0dd9230..b4fe004d9 100644
--- a/src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs
+++ b/src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs
@@ -137,7 +137,8 @@ impl ReduceTo<BiconnectivityAugmentation<SimpleGraph, i32>> for HamiltonianCircu
         }
 
         // Budget = n (exactly enough for n weight-1 edges)
-        let budget = n as i32;
+        let budget = i64::try_from(n)
+            .expect("HamiltonianCircuit -> BiconnectivityAugmentation budget must fit i64");
 
         let target = BiconnectivityAugmentation::new(initial_graph, potential_weights, budget);
 
diff --git a/src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs b/src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs
index e4b87c770..52d37e9fb 100644
--- a/src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs
+++ b/src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs
@@ -99,7 +99,8 @@ impl ReduceTo<StrongConnectivityAugmentation<i32>> for HamiltonianCircuit<Simple
             }
         }
 
-        let bound = n as i32;
+        let bound = i64::try_from(n)
+            .expect("HamiltonianCircuit -> StrongConnectivityAugmentation bound must fit i64");
         let target = StrongConnectivityAugmentation::new(graph, candidate_arcs, bound);
 
         ReductionHamiltonianCircuitToStrongConnectivityAugmentation { target, n }
diff --git a/src/rules/ksatisfiability_acyclicpartition.rs b/src/rules/ksatisfiability_acyclicpartition.rs
index 8b074ca22..66fadddf5 100644
--- a/src/rules/ksatisfiability_acyclicpartition.rs
+++ b/src/rules/ksatisfiability_acyclicpartition.rs
@@ -72,14 +72,10 @@ impl ReductionPartitionToAcyclicPartition {
             DirectedGraph::new(num_elements + 2, arcs),
             vertex_weights,
             arc_costs,
-            u64_to_i32(
-                weight_bound,
-                "Partition -> AcyclicPartition requires weight bound to fit in i32",
-            ),
-            usize_to_i32(
-                num_elements,
-                "Partition -> AcyclicPartition requires num_elements to fit in i32",
-            ),
+            i64::try_from(weight_bound)
+                .expect("Partition -> AcyclicPartition weight bound must fit in i64"),
+            i64::try_from(num_elements)
+                .expect("Partition -> AcyclicPartition cost bound must fit in i64"),
         );
 
         Self {
@@ -159,10 +155,6 @@ fn u64_to_i32(value: u64, context: &str) -> i32 {
     i32::try_from(value).expect(context)
 }
 
-fn usize_to_i32(value: usize, context: &str) -> i32 {
-    i32::try_from(value).expect(context)
-}
-
 #[reduction(
     overhead = {
         num_vertices = "2 * num_vars + 2 * num_clauses + 3",
diff --git a/src/rules/ksatisfiability_decisionminimumvertexcover.rs b/src/rules/ksatisfiability_decisionminimumvertexcover.rs
index dd22cacce..d945aed0d 100644
--- a/src/rules/ksatisfiability_decisionminimumvertexcover.rs
+++ b/src/rules/ksatisfiability_decisionminimumvertexcover.rs
@@ -50,8 +50,12 @@ impl ReduceTo<Decision<MinimumVertexCover<SimpleGraph, i32>>> for KSatisfiabilit
         let base_reduction = <KSatisfiability<K3> as ReduceTo<
             MinimumVertexCover<SimpleGraph, i32>,
         >>::reduce_to(self);
-        let bound = i32::try_from(self.num_vars() + 2 * self.num_clauses())
-            .expect("decision minimum vertex cover bound must fit in i32");
+        let bound = self
+            .num_clauses()
+            .checked_mul(2)
+            .and_then(|value| value.checked_add(self.num_vars()))
+            .and_then(|value| i64::try_from(value).ok())
+            .expect("decision minimum vertex cover bound must fit in i64");
         let target = Decision::new(base_reduction.target_problem().clone(), bound);
 
         Reduction3SATToDecisionMVC {
diff --git a/src/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/rules/ksatisfiability_oneinthreesatisfiability.rs
index b26034708..f84b3abbb 100644
--- a/src/rules/ksatisfiability_oneinthreesatisfiability.rs
+++ b/src/rules/ksatisfiability_oneinthreesatisfiability.rs
@@ -1,6 +1,8 @@
 //! Reduction from KSatisfiability (3-SAT) to One-In-Three Satisfiability.
 
-use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability};
+use crate::models::formula::{
+    CNFClause, KSatisfiability, OneInThreeSatisfiability, SatVariableAllocator,
+};
 use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 use crate::variant::K3;
@@ -38,33 +40,44 @@ impl ReduceTo<OneInThreeSatisfiability> for KSatisfiability<K3> {
 
     fn reduce_to(&self) -> Self::Result {
         let source_num_vars = self.num_vars();
-        let z_false = source_num_vars as i32 + 1;
-        let z_true = source_num_vars as i32 + 2;
-        let mut next_var = source_num_vars as i32 + 3;
-
-        let mut clauses = Vec::with_capacity(1 + 5 * self.num_clauses());
+        let mut variables = SatVariableAllocator::new(
+            "KSatisfiability -> OneInThreeSatisfiability",
+            source_num_vars,
+        )
+        .unwrap_or_else(|message| panic!("{message}"));
+        let sentinels = variables
+            .allocate_many(2)
+            .unwrap_or_else(|message| panic!("{message}"));
+        let z_false = sentinels[0];
+        let z_true = sentinels[1];
+
+        let capacity = self
+            .num_clauses()
+            .checked_mul(5)
+            .and_then(|count| count.checked_add(1))
+            .expect("KSatisfiability -> OneInThreeSatisfiability clause count overflow");
+        let mut clauses = Vec::with_capacity(capacity);
         clauses.push(CNFClause::new(vec![z_false, z_false, z_true]));
 
         for clause in self.clauses() {
             let [l1, l2, l3] = clause.literals.as_slice() else {
                 unreachable!("K3 clauses must have exactly three literals");
             };
-            let a = next_var;
-            let b = next_var + 1;
-            let c = next_var + 2;
-            let d = next_var + 3;
-            let e = next_var + 4;
-            let f = next_var + 5;
-            next_var += 6;
-
-            clauses.push(CNFClause::new(vec![*l1, a, d]));
-            clauses.push(CNFClause::new(vec![*l2, b, d]));
-            clauses.push(CNFClause::new(vec![a, b, e]));
-            clauses.push(CNFClause::new(vec![c, d, f]));
-            clauses.push(CNFClause::new(vec![*l3, c, z_false]));
+            let allocated = variables
+                .allocate_many(6)
+                .unwrap_or_else(|message| panic!("{message}"));
+            let [a, b, c, d, e, f] = allocated.as_slice() else {
+                unreachable!("six variables were allocated")
+            };
+
+            clauses.push(CNFClause::new(vec![*l1, *a, *d]));
+            clauses.push(CNFClause::new(vec![*l2, *b, *d]));
+            clauses.push(CNFClause::new(vec![*a, *b, *e]));
+            clauses.push(CNFClause::new(vec![*c, *d, *f]));
+            clauses.push(CNFClause::new(vec![*l3, *c, z_false]));
         }
 
-        let target = OneInThreeSatisfiability::new((next_var - 1) as usize, clauses);
+        let target = OneInThreeSatisfiability::new(variables.num_vars(), clauses);
 
         Reduction3SATToOneInThreeSAT {
             source_num_vars,
diff --git a/src/rules/ksatisfiability_timetabledesign.rs b/src/rules/ksatisfiability_timetabledesign.rs
index d7a005898..cb02c5f97 100644
--- a/src/rules/ksatisfiability_timetabledesign.rs
+++ b/src/rules/ksatisfiability_timetabledesign.rs
@@ -20,7 +20,7 @@
 //! graph; the colors on the two special variable edges recover the satisfying
 //! truth assignment.
 
-use crate::models::formula::{CNFClause, KSatisfiability};
+use crate::models::formula::{CNFClause, KSatisfiability, SatVariableAllocator};
 use crate::models::misc::TimetableDesign;
 use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
@@ -128,7 +128,7 @@ pub struct Reduction3SATToTimetableDesign {
 }
 
 fn literal_var_index(literal: i32) -> usize {
-    literal.unsigned_abs() as usize - 1
+    usize::try_from(literal.unsigned_abs()).expect("SAT literal magnitude must fit usize") - 1
 }
 
 #[cfg(any(test, feature = "example-db"))]
@@ -203,7 +203,11 @@ fn normalize_formula(source: &KSatisfiability<K3>) -> NormalizedFormula {
     let (mut clauses, pure_assignments) = eliminate_pure_literals(source);
     let source_num_vars = source.num_vars();
     let mut transformed_to_original = Vec::new();
-    let mut next_var = source_num_vars + 1;
+    let mut variables = SatVariableAllocator::new(
+        "KSatisfiability -> TimetableDesign normalization",
+        source_num_vars,
+    )
+    .unwrap_or_else(|message| panic!("{message}"));
 
     for original_var in 1..=source_num_vars {
         let mut occurrences = Vec::new();
@@ -220,41 +224,38 @@ fn normalize_formula(source: &KSatisfiability<K3>) -> NormalizedFormula {
         }
 
         if occurrences.len() <= 3 {
-            let replacement = next_var;
-            next_var += 1;
+            let replacement = variables
+                .allocate()
+                .unwrap_or_else(|message| panic!("{message}"));
             transformed_to_original.push(original_var - 1);
             for (clause_idx, lit_idx, is_positive) in occurrences {
                 clauses[clause_idx].literals[lit_idx] = if is_positive {
-                    replacement as i32
+                    replacement
                 } else {
-                    -(replacement as i32)
+                    -replacement
                 };
             }
             continue;
         }
 
-        let replacements: Vec<usize> = (0..occurrences.len())
-            .map(|_| {
-                let id = next_var;
-                next_var += 1;
-                transformed_to_original.push(original_var - 1);
-                id
-            })
-            .collect();
+        let replacements = variables
+            .allocate_many(occurrences.len())
+            .unwrap_or_else(|message| panic!("{message}"));
+        transformed_to_original.extend(std::iter::repeat_n(original_var - 1, replacements.len()));
 
         for ((clause_idx, lit_idx, is_positive), replacement) in
             occurrences.into_iter().zip(replacements.iter().copied())
         {
             clauses[clause_idx].literals[lit_idx] = if is_positive {
-                replacement as i32
+                replacement
             } else {
-                -(replacement as i32)
+                -replacement
             };
         }
 
         for idx in 0..replacements.len() {
-            let current = replacements[idx] as i32;
-            let next = replacements[(idx + 1) % replacements.len()] as i32;
+            let current = replacements[idx];
+            let next = replacements[(idx + 1) % replacements.len()];
             clauses.push(CNFClause::new(vec![current, -next]));
         }
     }
@@ -262,13 +263,16 @@ fn normalize_formula(source: &KSatisfiability<K3>) -> NormalizedFormula {
     for clause in &mut clauses {
         for literal in &mut clause.literals {
             let sign = if *literal < 0 { -1 } else { 1 };
-            let temp_var = literal.unsigned_abs() as usize;
+            let temp_var = usize::try_from(literal.unsigned_abs())
+                .expect("SAT literal magnitude must fit usize");
             debug_assert!(
                 temp_var > source_num_vars,
                 "all residual literals should have been replaced by transformed variables"
             );
             let compact_var = temp_var - source_num_vars;
-            *literal = sign * compact_var as i32;
+            *literal = sign
+                * i32::try_from(compact_var)
+                    .expect("checked normalized SAT variable count fits i32");
         }
     }
 
diff --git a/src/rules/minimumvertexcover_comparativecontainment.rs b/src/rules/minimumvertexcover_comparativecontainment.rs
index 3b1e13333..ebbc6f1d1 100644
--- a/src/rules/minimumvertexcover_comparativecontainment.rs
+++ b/src/rules/minimumvertexcover_comparativecontainment.rs
@@ -111,7 +111,8 @@ impl ReduceTo<ComparativeContainment<i32>> for Decision<MinimumVertexCover<Simpl
         // covers every edge), so the answer is YES regardless of the graph.
         // Emit an empty target instance (universe size 0, no R/S sets); its
         // unique configuration is trivially satisfying.
-        if raw_bound >= num_vertices as i32 {
+        if i128::from(raw_bound) >= i128::try_from(num_vertices).expect("usize always fits in i128")
+        {
             let target = ComparativeContainment::with_weights(
                 0,
                 Vec::new(),
diff --git a/src/rules/sat_ksat.rs b/src/rules/sat_ksat.rs
index 2bf711699..a72036704 100644
--- a/src/rules/sat_ksat.rs
+++ b/src/rules/sat_ksat.rs
@@ -6,7 +6,7 @@
 //!
 //! K-SAT -> SAT: Trivial embedding (K-SAT is a special case of SAT)
 
-use crate::models::formula::{CNFClause, KSatisfiability, Satisfiability};
+use crate::models::formula::{CNFClause, KSatisfiability, SatVariableAllocator, Satisfiability};
 use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 use crate::variant::{KValue, K2, K3, KN};
@@ -55,16 +55,12 @@ impl<K: KValue> ReductionResult for ReductionSATToKSAT<K> {
 /// * `k` - Target number of literals per clause
 /// * `clause` - The clause to add
 /// * `result_clauses` - Output vector to append clauses to
-/// * `next_var` - Next available variable number (1-indexed)
-///
-/// # Returns
-/// Updated next_var after any ancilla variables are created
 fn add_clause_to_ksat(
     k: usize,
     clause: &CNFClause,
     result_clauses: &mut Vec<CNFClause>,
-    mut next_var: i32,
-) -> i32 {
+    variables: &mut SatVariableAllocator,
+) -> Result<(), String> {
     let len = clause.len();
 
     if len == k {
@@ -74,25 +70,23 @@ fn add_clause_to_ksat(
         // Too few literals: pad with ancilla variables
         // Create both positive and negative versions to maintain satisfiability
         // (a v b) with k=3 becomes (a v b v x) AND (a v b v -x)
-        let ancilla = next_var;
-        next_var += 1;
+        let ancilla = variables.allocate()?;
 
         // Add clause with positive ancilla
         let mut lits_pos = clause.literals.clone();
         lits_pos.push(ancilla);
-        next_var = add_clause_to_ksat(k, &CNFClause::new(lits_pos), result_clauses, next_var);
+        add_clause_to_ksat(k, &CNFClause::new(lits_pos), result_clauses, variables)?;
 
         // Add clause with negative ancilla
         let mut lits_neg = clause.literals.clone();
         lits_neg.push(-ancilla);
-        next_var = add_clause_to_ksat(k, &CNFClause::new(lits_neg), result_clauses, next_var);
+        add_clause_to_ksat(k, &CNFClause::new(lits_neg), result_clauses, variables)?;
     } else {
         // Too many literals: split using ancilla variable
         // (a v b v c v d) with k=3 becomes (a v b v x) AND (-x v c v d)
         assert!(k >= 3, "K must be at least 3 for splitting");
 
-        let ancilla = next_var;
-        next_var += 1;
+        let ancilla = variables.allocate()?;
 
         // First clause: first k-1 literals + positive ancilla
         let mut first_lits: Vec<i32> = clause.literals[..k - 1].to_vec();
@@ -105,10 +99,10 @@ fn add_clause_to_ksat(
         let remaining_clause = CNFClause::new(remaining_lits);
 
         // Recursively process the remaining clause
-        next_var = add_clause_to_ksat(k, &remaining_clause, result_clauses, next_var);
+        add_clause_to_ksat(k, &remaining_clause, result_clauses, variables)?;
     }
 
-    next_var
+    Ok(())
 }
 
 /// Implementation of SAT -> K-SAT reduction.
@@ -128,16 +122,17 @@ macro_rules! impl_sat_to_ksat {
             fn reduce_to(&self) -> Self::Result {
                 let source_num_vars = self.num_vars();
                 let mut result_clauses = Vec::new();
-                let mut next_var = (source_num_vars + 1) as i32; // 1-indexed
+                let mut variables = SatVariableAllocator::new(
+                    "Satisfiability -> KSatisfiability",
+                    source_num_vars,
+                ).unwrap_or_else(|message| panic!("{message}"));
 
                 for clause in self.clauses() {
-                    next_var = add_clause_to_ksat($k, clause, &mut result_clauses, next_var);
+                    add_clause_to_ksat($k, clause, &mut result_clauses, &mut variables)
+                        .unwrap_or_else(|message| panic!("{message}"));
                 }
 
-                // Calculate total number of variables (original + ancillas)
-                let total_vars = (next_var - 1) as usize;
-
-                let target = KSatisfiability::<$ktype>::new(total_vars, result_clauses);
+                let target = KSatisfiability::<$ktype>::new(variables.num_vars(), result_clauses);
 
                 ReductionSATToKSAT {
                     source_num_vars,
diff --git a/src/rules/satisfiability_maximum2satisfiability.rs b/src/rules/satisfiability_maximum2satisfiability.rs
index 8b375f917..c245ac17f 100644
--- a/src/rules/satisfiability_maximum2satisfiability.rs
+++ b/src/rules/satisfiability_maximum2satisfiability.rs
@@ -1,6 +1,8 @@
 //! Reduction from Satisfiability to Maximum 2-Satisfiability.
 
-use crate::models::formula::{CNFClause, Maximum2Satisfiability, Satisfiability};
+use crate::models::formula::{
+    CNFClause, Maximum2Satisfiability, SatVariableAllocator, Satisfiability,
+};
 use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 
@@ -29,19 +31,22 @@ impl ReductionResult for ReductionSatisfiabilityToMaximum2Satisfiability {
     }
 }
 
-fn add_normalized_clause(clause: &CNFClause, next_var: &mut i32, normalized: &mut Vec<CNFClause>) {
+fn add_normalized_clause(
+    clause: &CNFClause,
+    variables: &mut SatVariableAllocator,
+    normalized: &mut Vec<CNFClause>,
+) -> Result<(), String> {
     match clause.len() {
         0 => {
-            let y = *next_var;
-            *next_var += 1;
+            let y = variables.allocate()?;
             normalized.push(CNFClause::new(vec![y, y, y]));
             normalized.push(CNFClause::new(vec![-y, -y, -y]));
         }
         1 => {
             let l1 = clause.literals[0];
-            let y = *next_var;
-            let z = *next_var + 1;
-            *next_var += 2;
+            let allocated = variables.allocate_many(2)?;
+            let y = allocated[0];
+            let z = allocated[1];
             normalized.push(CNFClause::new(vec![l1, y, z]));
             normalized.push(CNFClause::new(vec![l1, y, -z]));
             normalized.push(CNFClause::new(vec![l1, -y, z]));
@@ -50,16 +55,14 @@ fn add_normalized_clause(clause: &CNFClause, next_var: &mut i32, normalized: &mu
         2 => {
             let l1 = clause.literals[0];
             let l2 = clause.literals[1];
-            let y = *next_var;
-            *next_var += 1;
+            let y = variables.allocate()?;
             normalized.push(CNFClause::new(vec![l1, l2, y]));
             normalized.push(CNFClause::new(vec![l1, l2, -y]));
         }
         3 => normalized.push(clause.clone()),
         k => {
             let literals = &clause.literals;
-            let y_vars: Vec<i32> = (*next_var..*next_var + (k as i32 - 3)).collect();
-            *next_var += k as i32 - 3;
+            let y_vars = variables.allocate_many(k - 3)?;
 
             normalized.push(CNFClause::new(vec![literals[0], literals[1], y_vars[0]]));
             for i in 1..k - 3 {
@@ -76,6 +79,7 @@ fn add_normalized_clause(clause: &CNFClause, next_var: &mut i32, normalized: &mu
             ]));
         }
     }
+    Ok(())
 }
 
 fn add_gjs_gadget(clause: &CNFClause, w: i32, target_clauses: &mut Vec<CNFClause>) {
@@ -106,20 +110,28 @@ impl ReduceTo<Maximum2Satisfiability> for Satisfiability {
 
     fn reduce_to(&self) -> Self::Result {
         let mut normalized = Vec::new();
-        let mut next_var = self.num_vars() as i32 + 1;
+        let mut variables =
+            SatVariableAllocator::new("Satisfiability -> Maximum2Satisfiability", self.num_vars())
+                .unwrap_or_else(|message| panic!("{message}"));
 
         for clause in self.clauses() {
-            add_normalized_clause(clause, &mut next_var, &mut normalized);
+            add_normalized_clause(clause, &mut variables, &mut normalized)
+                .unwrap_or_else(|message| panic!("{message}"));
         }
 
-        let mut target_clauses = Vec::with_capacity(normalized.len() * 10);
+        let capacity = normalized
+            .len()
+            .checked_mul(10)
+            .expect("Satisfiability -> Maximum2Satisfiability clause count overflow");
+        let mut target_clauses = Vec::with_capacity(capacity);
         for clause in &normalized {
-            let w = next_var;
-            next_var += 1;
+            let w = variables
+                .allocate()
+                .unwrap_or_else(|message| panic!("{message}"));
             add_gjs_gadget(clause, w, &mut target_clauses);
         }
 
-        let target = Maximum2Satisfiability::new((next_var - 1) as usize, target_clauses);
+        let target = Maximum2Satisfiability::new(variables.num_vars(), target_clauses);
 
         ReductionSatisfiabilityToMaximum2Satisfiability {
             target,
diff --git a/src/rules/satisfiability_naesatisfiability.rs b/src/rules/satisfiability_naesatisfiability.rs
index 0f90f23bb..39a777bd5 100644
--- a/src/rules/satisfiability_naesatisfiability.rs
+++ b/src/rules/satisfiability_naesatisfiability.rs
@@ -7,7 +7,7 @@
 //! has at least one false literal (the sentinel itself when s=false, or
 //! the complement of the original satisfied literal when s=true).
 
-use crate::models::formula::{CNFClause, NAESatisfiability, Satisfiability};
+use crate::models::formula::{CNFClause, NAESatisfiability, SatVariableAllocator, Satisfiability};
 use crate::reduction;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 
@@ -53,8 +53,11 @@ impl ReduceTo<NAESatisfiability> for Satisfiability {
 
     fn reduce_to(&self) -> Self::Result {
         let n = self.num_vars();
-        // Sentinel variable has 0-indexed position n, so its 1-indexed literal is n+1.
-        let sentinel_lit = (n + 1) as i32;
+        let mut variables = SatVariableAllocator::new("Satisfiability -> NAESatisfiability", n)
+            .unwrap_or_else(|message| panic!("{message}"));
+        let sentinel_lit = variables
+            .allocate()
+            .unwrap_or_else(|message| panic!("{message}"));
 
         let nae_clauses: Vec<CNFClause> = self
             .clauses()
@@ -72,7 +75,7 @@ impl ReduceTo<NAESatisfiability> for Satisfiability {
             })
             .collect();
 
-        let target = NAESatisfiability::new(n + 1, nae_clauses);
+        let target = NAESatisfiability::new(variables.num_vars(), nae_clauses);
 
         ReductionSATToNAESAT {
             source_num_vars: n,
diff --git a/src/solvers/decision_search.rs b/src/solvers/decision_search.rs
index d69a9804a..7b320893c 100644
--- a/src/solvers/decision_search.rs
+++ b/src/solvers/decision_search.rs
@@ -16,9 +16,9 @@ where
     BruteForce::new().solve(problem).0
 }
 
-fn solve_via_decision_min<P>(problem: &P, lower: i32, upper: i32) -> Option<i32>
+fn solve_via_decision_min<P>(problem: &P, lower: i64, upper: i64) -> Option<i64>
 where
-    P: DecisionProblemMeta + Problem<Value = Min<i32>> + Clone,
+    P: DecisionProblemMeta + Problem<Value = Min<i64>> + Clone,
 {
     if lower > upper {
         return None;
@@ -42,9 +42,9 @@ where
     Some(lo)
 }
 
-fn solve_via_decision_max<P>(problem: &P, lower: i32, upper: i32) -> Option<i32>
+fn solve_via_decision_max<P>(problem: &P, lower: i64, upper: i64) -> Option<i64>
 where
-    P: DecisionProblemMeta + Problem<Value = Max<i32>> + Clone,
+    P: DecisionProblemMeta + Problem<Value = Max<i64>> + Clone,
 {
     if lower > upper {
         return None;
@@ -70,15 +70,15 @@ where
 
 #[doc(hidden)]
 pub trait DecisionSearchValue:
-    OptimizationValue<Inner = i32> + Clone + fmt::Debug + Serialize + DeserializeOwned
+    OptimizationValue<Inner = i64> + Clone + fmt::Debug + Serialize + DeserializeOwned
 {
-    fn solve_problem<P>(problem: &P, lower: i32, upper: i32) -> Option<i32>
+    fn solve_problem<P>(problem: &P, lower: i64, upper: i64) -> Option<i64>
     where
         P: DecisionProblemMeta + Problem<Value = Self> + Clone;
 }
 
-impl DecisionSearchValue for Min<i32> {
-    fn solve_problem<P>(problem: &P, lower: i32, upper: i32) -> Option<i32>
+impl DecisionSearchValue for Min<i64> {
+    fn solve_problem<P>(problem: &P, lower: i64, upper: i64) -> Option<i64>
     where
         P: DecisionProblemMeta + Problem<Value = Self> + Clone,
     {
@@ -86,8 +86,8 @@ impl DecisionSearchValue for Min<i32> {
     }
 }
 
-impl DecisionSearchValue for Max<i32> {
-    fn solve_problem<P>(problem: &P, lower: i32, upper: i32) -> Option<i32>
+impl DecisionSearchValue for Max<i64> {
+    fn solve_problem<P>(problem: &P, lower: i64, upper: i64) -> Option<i64>
     where
         P: DecisionProblemMeta + Problem<Value = Self> + Clone,
     {
@@ -96,7 +96,7 @@ impl DecisionSearchValue for Max<i32> {
 }
 
 /// Recover an optimization value by querying the problem's decision wrapper.
-pub fn solve_via_decision<P>(problem: &P, lower: i32, upper: i32) -> Option<i32>
+pub fn solve_via_decision<P>(problem: &P, lower: i64, upper: i64) -> Option<i64>
 where
     P: DecisionProblemMeta + Clone,
     P::Value: DecisionSearchValue,
diff --git a/src/types.rs b/src/types.rs
index cc859423b..e661e04b9 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -32,8 +32,9 @@ impl<T> NumericSize for T where
 /// Maps a weight element to its sum/metric type.
 ///
 /// This decouples the per-element weight type from the accumulation type.
-/// For concrete weights (`i32`, `f64`), `Sum` is the same type.
-/// For the unit weight `One`, `Sum = i32`.
+/// Exact integer weights use a wider accumulation type: `i32` and the unit
+/// weight [`One`] both use `i64`. Approximate `f64` weights continue to sum
+/// into `f64`.
 pub trait WeightElement: Clone + Default + 'static {
     /// The numeric type used for sums and comparisons.
     type Sum: NumericSize;
@@ -44,10 +45,10 @@ pub trait WeightElement: Clone + Default + 'static {
 }
 
 impl WeightElement for i32 {
-    type Sum = i32;
+    type Sum = i64;
     const IS_UNIT: bool = false;
-    fn to_sum(&self) -> i32 {
-        *self
+    fn to_sum(&self) -> i64 {
+        i64::from(*self)
     }
 }
 
@@ -62,7 +63,7 @@ impl WeightElement for f64 {
 /// The constant 1. Unit weight for unweighted problems.
 ///
 /// When used as the weight type parameter `W`, indicates that all weights
-/// are uniformly 1. `One::to_sum()` returns `1i32`.
+/// are uniformly 1. `One::to_sum()` returns `1i64`.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
 pub struct One;
 
@@ -142,9 +143,9 @@ impl<'de> Deserialize<'de> for One {
 }
 
 impl WeightElement for One {
-    type Sum = i32;
+    type Sum = i64;
     const IS_UNIT: bool = true;
-    fn to_sum(&self) -> i32 {
+    fn to_sum(&self) -> i64 {
         1
     }
 }
diff --git a/src/unit_tests/models/formula/one_in_three_satisfiability.rs b/src/unit_tests/models/formula/one_in_three_satisfiability.rs
index e20220e2e..c54ca0eb8 100644
--- a/src/unit_tests/models/formula/one_in_three_satisfiability.rs
+++ b/src/unit_tests/models/formula/one_in_three_satisfiability.rs
@@ -118,7 +118,7 @@ fn test_one_in_three_satisfiability_wrong_clause_width() {
 }
 
 #[test]
-#[should_panic(expected = "outside range")]
+#[should_panic(expected = "allowed variable numbers are 1..=2")]
 fn test_one_in_three_satisfiability_variable_out_of_range() {
     OneInThreeSatisfiability::new(2, vec![CNFClause::new(vec![1, 2, 3])]);
 }
diff --git a/src/unit_tests/models/formula/planar_3_satisfiability.rs b/src/unit_tests/models/formula/planar_3_satisfiability.rs
index ccbdffc8f..47b6a8500 100644
--- a/src/unit_tests/models/formula/planar_3_satisfiability.rs
+++ b/src/unit_tests/models/formula/planar_3_satisfiability.rs
@@ -135,7 +135,7 @@ fn test_planar_3_satisfiability_wrong_clause_width() {
 }
 
 #[test]
-#[should_panic(expected = "outside range")]
+#[should_panic(expected = "allowed variable numbers are 1..=2")]
 fn test_planar_3_satisfiability_variable_out_of_range() {
     Planar3Satisfiability::new(2, vec![CNFClause::new(vec![1, 2, 3])]);
 }
diff --git a/src/unit_tests/models/formula/qbf.rs b/src/unit_tests/models/formula/qbf.rs
index 136cc967d..3e408a0f0 100644
--- a/src/unit_tests/models/formula/qbf.rs
+++ b/src/unit_tests/models/formula/qbf.rs
@@ -133,8 +133,8 @@ fn test_qbf_zero_vars() {
 
 #[test]
 fn test_qbf_zero_vars_unsat() {
-    // Zero variables, but a clause that refers to var 1 (unsatisfiable)
-    let problem = QuantifiedBooleanFormulas::new(0, vec![], vec![CNFClause::new(vec![1])]);
+    // An empty clause is false without referring to a nonexistent variable.
+    let problem = QuantifiedBooleanFormulas::new(0, vec![], vec![CNFClause::new(vec![])]);
     assert!(!problem.evaluate(&[]));
     assert!(!problem.is_true());
 }
diff --git a/src/unit_tests/models/formula/sat.rs b/src/unit_tests/models/formula/sat.rs
index 29ddad85a..392a282ba 100644
--- a/src/unit_tests/models/formula/sat.rs
+++ b/src/unit_tests/models/formula/sat.rs
@@ -3,6 +3,33 @@ use crate::solvers::BruteForce;
 use crate::traits::Problem;
 include!("../../jl_helpers.rs");
 
+#[test]
+fn test_sat_variable_allocator_numeric_boundaries() {
+    let mut allocator = SatVariableAllocator::new("test reduction", i32::MAX as usize - 1)
+        .expect("largest valid starting count");
+    assert_eq!(allocator.allocate().unwrap(), i32::MAX);
+    assert_eq!(allocator.num_vars(), i32::MAX as usize);
+
+    let error = allocator.allocate().unwrap_err();
+    assert!(error.contains("test reduction"));
+    assert!(error.contains("limited to 2147483647"));
+}
+
+#[test]
+fn test_sat_variable_allocator_batch_numeric_boundaries() {
+    let mut exact = SatVariableAllocator::new("exact batch", i32::MAX as usize - 2).unwrap();
+    assert_eq!(
+        exact.allocate_many(2).unwrap(),
+        vec![i32::MAX - 1, i32::MAX]
+    );
+    assert_eq!(exact.num_vars(), i32::MAX as usize);
+
+    let mut overflow = SatVariableAllocator::new("overflow batch", i32::MAX as usize - 1).unwrap();
+    let error = overflow.allocate_many(2).unwrap_err();
+    assert!(error.contains("cannot allocate 2 auxiliary variables"));
+    assert_eq!(overflow.num_vars(), i32::MAX as usize - 1);
+}
+
 #[test]
 fn test_cnf_clause_creation() {
     let clause = CNFClause::new(vec![1, -2, 3]);
@@ -106,7 +133,7 @@ fn test_empty_formula_zero_vars_solver() {
 
 #[test]
 fn test_zero_vars_unsat_solver() {
-    let problem = Satisfiability::new(0, vec![CNFClause::new(vec![1])]);
+    let problem = Satisfiability::new(0, vec![CNFClause::new(vec![])]);
     let solver = BruteForce::new();
 
     assert_eq!(solver.find_witness(&problem), None);
diff --git a/src/unit_tests/models/graph/max_cut.rs b/src/unit_tests/models/graph/max_cut.rs
index dcfadc6e6..b75ce5bdf 100644
--- a/src/unit_tests/models/graph/max_cut.rs
+++ b/src/unit_tests/models/graph/max_cut.rs
@@ -104,7 +104,7 @@ fn test_jl_parity_evaluation() {
         for eval in instance["evaluations"].as_array().unwrap() {
             let config = jl_parse_config(&eval["config"]);
             let result = problem.evaluate(&config);
-            let jl_size = eval["size"].as_i64().unwrap() as i32;
+            let jl_size = eval["size"].as_i64().unwrap();
             assert!(result.is_valid(), "MaxCut should always be valid");
             assert_eq!(
                 result.unwrap(),
diff --git a/src/unit_tests/models/graph/maximal_is.rs b/src/unit_tests/models/graph/maximal_is.rs
index 06f2b3566..d0f1a1f1c 100644
--- a/src/unit_tests/models/graph/maximal_is.rs
+++ b/src/unit_tests/models/graph/maximal_is.rs
@@ -141,7 +141,7 @@ fn test_jl_parity_evaluation() {
                 config
             );
             if jl_valid {
-                let jl_size = eval["size"].as_i64().unwrap() as i32;
+                let jl_size = eval["size"].as_i64().unwrap();
                 assert_eq!(
                     result.unwrap(),
                     jl_size,
diff --git a/src/unit_tests/models/graph/maximum_independent_set.rs b/src/unit_tests/models/graph/maximum_independent_set.rs
index 4362cfc39..9053054c9 100644
--- a/src/unit_tests/models/graph/maximum_independent_set.rs
+++ b/src/unit_tests/models/graph/maximum_independent_set.rs
@@ -139,7 +139,7 @@ fn test_jl_parity_evaluation() {
                 config
             );
             if jl_valid {
-                let jl_size = eval["size"].as_i64().unwrap() as i32;
+                let jl_size = eval["size"].as_i64().unwrap();
                 assert_eq!(
                     result.unwrap(),
                     jl_size,
diff --git a/src/unit_tests/models/graph/maximum_matching.rs b/src/unit_tests/models/graph/maximum_matching.rs
index 17c170e8c..d01e67dfc 100644
--- a/src/unit_tests/models/graph/maximum_matching.rs
+++ b/src/unit_tests/models/graph/maximum_matching.rs
@@ -132,7 +132,7 @@ fn test_jl_parity_evaluation() {
                 config
             );
             if jl_valid {
-                let jl_size = eval["size"].as_i64().unwrap() as i32;
+                let jl_size = eval["size"].as_i64().unwrap();
                 assert_eq!(
                     result.unwrap(),
                     jl_size,
diff --git a/src/unit_tests/models/graph/minimum_dominating_set.rs b/src/unit_tests/models/graph/minimum_dominating_set.rs
index a1665a701..b80eaedb5 100644
--- a/src/unit_tests/models/graph/minimum_dominating_set.rs
+++ b/src/unit_tests/models/graph/minimum_dominating_set.rs
@@ -138,7 +138,7 @@ fn test_jl_parity_evaluation() {
                 config
             );
             if jl_valid {
-                let jl_size = eval["size"].as_i64().unwrap() as i32;
+                let jl_size = eval["size"].as_i64().unwrap();
                 assert_eq!(
                     result.unwrap(),
                     jl_size,
diff --git a/src/unit_tests/models/graph/minimum_vertex_cover.rs b/src/unit_tests/models/graph/minimum_vertex_cover.rs
index 39f052644..2fb7b22a1 100644
--- a/src/unit_tests/models/graph/minimum_vertex_cover.rs
+++ b/src/unit_tests/models/graph/minimum_vertex_cover.rs
@@ -122,7 +122,7 @@ fn test_jl_parity_evaluation() {
                 config
             );
             if jl_valid {
-                let jl_size = eval["size"].as_i64().unwrap() as i32;
+                let jl_size = eval["size"].as_i64().unwrap();
                 assert_eq!(
                     result.unwrap(),
                     jl_size,
diff --git a/src/unit_tests/models/graph/spin_glass.rs b/src/unit_tests/models/graph/spin_glass.rs
index e5ff4fdea..82633c899 100644
--- a/src/unit_tests/models/graph/spin_glass.rs
+++ b/src/unit_tests/models/graph/spin_glass.rs
@@ -114,7 +114,7 @@ fn test_jl_parity_evaluation() {
             let jl_config = jl_parse_config(&eval["config"]);
             let config = jl_flip_config(&jl_config);
             let result = problem.evaluate(&config);
-            let jl_size = eval["size"].as_i64().unwrap() as i32;
+            let jl_size = eval["size"].as_i64().unwrap();
             assert!(result.is_valid(), "SpinGlass should always be valid");
             assert_eq!(
                 result.unwrap(),
diff --git a/src/unit_tests/models/set/maximum_set_packing.rs b/src/unit_tests/models/set/maximum_set_packing.rs
index 405d55d1b..3f5a67f48 100644
--- a/src/unit_tests/models/set/maximum_set_packing.rs
+++ b/src/unit_tests/models/set/maximum_set_packing.rs
@@ -115,7 +115,7 @@ fn test_jl_parity_evaluation() {
                 config
             );
             if jl_valid {
-                let jl_size = eval["size"].as_i64().unwrap() as i32;
+                let jl_size = eval["size"].as_i64().unwrap();
                 assert_eq!(
                     result.unwrap(),
                     jl_size,
diff --git a/src/unit_tests/models/set/minimum_set_covering.rs b/src/unit_tests/models/set/minimum_set_covering.rs
index c218fc56d..bee8eeed5 100644
--- a/src/unit_tests/models/set/minimum_set_covering.rs
+++ b/src/unit_tests/models/set/minimum_set_covering.rs
@@ -85,7 +85,7 @@ fn test_jl_parity_evaluation() {
                 config
             );
             if jl_valid {
-                let jl_size = eval["size"].as_i64().unwrap() as i32;
+                let jl_size = eval["size"].as_i64().unwrap();
                 assert_eq!(
                     result.unwrap(),
                     jl_size,
diff --git a/src/unit_tests/rules/decisionminimumdominatingset_minimumsummulticenter.rs b/src/unit_tests/rules/decisionminimumdominatingset_minimumsummulticenter.rs
index 93d768754..cb4f3f056 100644
--- a/src/unit_tests/rules/decisionminimumdominatingset_minimumsummulticenter.rs
+++ b/src/unit_tests/rules/decisionminimumdominatingset_minimumsummulticenter.rs
@@ -9,7 +9,7 @@ use crate::types::{One, Or};
 fn decision_mds(
     num_vertices: usize,
     edges: &[(usize, usize)],
-    k: i32,
+    k: i64,
 ) -> Decision<MinimumDominatingSet<SimpleGraph, One>> {
     Decision::new(
         MinimumDominatingSet::new(
@@ -80,7 +80,8 @@ fn test_decisionminimumdominatingset_to_minimumsummulticenter_closed_loop_no_ins
         "target should still have optimal K-center placements"
     );
 
-    let threshold = source.inner().graph().num_vertices() as i32 - source.k() as i32;
+    let threshold = i64::try_from(source.inner().graph().num_vertices()).unwrap()
+        - i64::try_from(source.k()).unwrap();
     for target_solution in target_solutions {
         let target_value = target.evaluate(&target_solution).unwrap();
         assert_eq!(target_value, 6);
diff --git a/src/unit_tests/rules/decisionminimumdominatingset_minmaxmulticenter.rs b/src/unit_tests/rules/decisionminimumdominatingset_minmaxmulticenter.rs
index 506524c70..ac8e93966 100644
--- a/src/unit_tests/rules/decisionminimumdominatingset_minmaxmulticenter.rs
+++ b/src/unit_tests/rules/decisionminimumdominatingset_minmaxmulticenter.rs
@@ -10,7 +10,7 @@ use crate::types::{One, Or};
 fn decision_mds(
     num_vertices: usize,
     edges: &[(usize, usize)],
-    k: i32,
+    k: i64,
 ) -> Decision<MinimumDominatingSet<SimpleGraph, One>> {
     Decision::new(
         MinimumDominatingSet::new(
diff --git a/src/unit_tests/rules/decisionminimumvertexcover_hamiltoniancircuit.rs b/src/unit_tests/rules/decisionminimumvertexcover_hamiltoniancircuit.rs
index db7b3a7bc..b2c19493c 100644
--- a/src/unit_tests/rules/decisionminimumvertexcover_hamiltoniancircuit.rs
+++ b/src/unit_tests/rules/decisionminimumvertexcover_hamiltoniancircuit.rs
@@ -10,7 +10,7 @@ fn decision_mvc(
     num_vertices: usize,
     edges: &[(usize, usize)],
     weights: &[i32],
-    k: i32,
+    k: i64,
 ) -> Decision<MinimumVertexCover<SimpleGraph, i32>> {
     Decision::new(
         MinimumVertexCover::new(
diff --git a/src/unit_tests/rules/exactcoverby3sets_boundeddiameterspanningtree.rs b/src/unit_tests/rules/exactcoverby3sets_boundeddiameterspanningtree.rs
index e25e3854d..6905c86b0 100644
--- a/src/unit_tests/rules/exactcoverby3sets_boundeddiameterspanningtree.rs
+++ b/src/unit_tests/rules/exactcoverby3sets_boundeddiameterspanningtree.rs
@@ -45,7 +45,7 @@ fn test_exactcoverby3sets_to_boundeddiameterspanningtree_structure() {
     // Diameter bound is always 4 in the canonical construction.
     assert_eq!(target.diameter_bound(), 4);
     // Weight bound B = 4q + m + 2.
-    let expected_weight_bound = (4 * q + m + 2) as i32;
+    let expected_weight_bound = i64::try_from(4 * q + m + 2).unwrap();
     assert_eq!(*target.weight_bound(), expected_weight_bound);
 
     // Verify the first two edges are the forced-center path with weight 1.
diff --git a/src/unit_tests/rules/hamiltoniancircuit_ruralpostman.rs b/src/unit_tests/rules/hamiltoniancircuit_ruralpostman.rs
index f6be3b713..c3a9e0862 100644
--- a/src/unit_tests/rules/hamiltoniancircuit_ruralpostman.rs
+++ b/src/unit_tests/rules/hamiltoniancircuit_ruralpostman.rs
@@ -108,7 +108,7 @@ fn test_hamiltoniancircuit_to_ruralpostman_nonhamiltonian_cost_gap() {
             metric.is_valid(),
             "best RPP solution should be a valid circuit"
         );
-        let two_n = 2 * n as i32;
+        let two_n = 2 * i64::try_from(n).unwrap();
         assert!(
             metric.unwrap() > two_n,
             "non-Hamiltonian source should give RPP cost > 2n={two_n}, got {}",
diff --git a/src/unit_tests/rules/maxcut_minimummatrixcover.rs b/src/unit_tests/rules/maxcut_minimummatrixcover.rs
index a0944aa25..79e213151 100644
--- a/src/unit_tests/rules/maxcut_minimummatrixcover.rs
+++ b/src/unit_tests/rules/maxcut_minimummatrixcover.rs
@@ -33,7 +33,7 @@ fn verify_identity(source: &MaxCut<SimpleGraph, i32>) {
         let Max(Some(cut)) = source.evaluate(&config) else {
             panic!("MaxCut must yield a finite cut for every config");
         };
-        let cut64 = cut as i64;
+        let cut64 = cut;
 
         assert_eq!(
             qf,
diff --git a/src/unit_tests/rules/maximum2satisfiability_maxcut.rs b/src/unit_tests/rules/maximum2satisfiability_maxcut.rs
index 5bbbaba45..55ab86955 100644
--- a/src/unit_tests/rules/maximum2satisfiability_maxcut.rs
+++ b/src/unit_tests/rules/maximum2satisfiability_maxcut.rs
@@ -65,7 +65,7 @@ fn test_maximum2satisfiability_to_maxcut_issue_affine_relation_on_all_partitions
             .map(|bit| (mask >> bit) & 1)
             .collect();
         let source_solution = reduction.extract_solution(&target_solution).unwrap();
-        let satisfied = source.evaluate(&source_solution).unwrap() as i32;
+        let satisfied = i64::try_from(source.evaluate(&source_solution).unwrap()).unwrap();
         let cut_weight = target.evaluate(&target_solution).unwrap();
 
         assert_eq!(
diff --git a/src/unit_tests/rules/minimumvertexcover_comparativecontainment.rs b/src/unit_tests/rules/minimumvertexcover_comparativecontainment.rs
index a5e3f7dcc..cba17eb04 100644
--- a/src/unit_tests/rules/minimumvertexcover_comparativecontainment.rs
+++ b/src/unit_tests/rules/minimumvertexcover_comparativecontainment.rs
@@ -10,7 +10,7 @@ use crate::traits::Problem;
 fn decision_mvc(
     num_vertices: usize,
     edges: &[(usize, usize)],
-    k: i32,
+    k: i64,
 ) -> Decision<MinimumVertexCover<SimpleGraph, i32>> {
     Decision::new(
         MinimumVertexCover::new(
diff --git a/src/unit_tests/rules/sat_ksat.rs b/src/unit_tests/rules/sat_ksat.rs
index 2eb0210d3..85841f0eb 100644
--- a/src/unit_tests/rules/sat_ksat.rs
+++ b/src/unit_tests/rules/sat_ksat.rs
@@ -244,14 +244,14 @@ fn test_sat_to_3sat_mixed_clause_types() {
 
 #[test]
 fn test_ksat_structure() {
-    let sat = Satisfiability::new(3, vec![CNFClause::new(vec![1, 2, 3, 4])]);
+    let sat = Satisfiability::new(4, vec![CNFClause::new(vec![1, 2, 3, 4])]);
 
     let reduction = ReduceTo::<KSatisfiability<K3>>::reduce_to(&sat);
     let ksat = reduction.target_problem();
 
     // K-SAT should preserve original variables plus auxiliary vars
     // A 4-literal clause requires 1 auxiliary variable for Tseitin
-    assert_eq!(ksat.num_vars(), 3 + 1); // Original vars + 1 auxiliary for Tseitin
+    assert_eq!(ksat.num_vars(), 4 + 1); // Original vars + 1 auxiliary for Tseitin
 }
 
 #[test]
diff --git a/tests/main.rs b/tests/main.rs
index 6f8e4c248..92586f779 100644
--- a/tests/main.rs
+++ b/tests/main.rs
@@ -8,6 +8,8 @@ mod integration;
 mod jl_parity;
 #[path = "suites/ksatisfiability_simultaneous_incongruences.rs"]
 mod ksatisfiability_simultaneous_incongruences;
+#[path = "suites/numeric_boundaries.rs"]
+mod numeric_boundaries;
 #[path = "suites/reductions.rs"]
 mod reductions;
 #[cfg(feature = "ilp-solver")]
diff --git a/tests/suites/numeric_boundaries.rs b/tests/suites/numeric_boundaries.rs
new file mode 100644
index 000000000..a543f55f0
--- /dev/null
+++ b/tests/suites/numeric_boundaries.rs
@@ -0,0 +1,104 @@
+use problemreductions::models::formula::{
+    CNFClause, KSatisfiability, Maximum2Satisfiability, NAESatisfiability,
+    OneInThreeSatisfiability, Planar3Satisfiability, QuantifiedBooleanFormulas, Quantifier,
+    Satisfiability,
+};
+use problemreductions::models::graph::MinimumDominatingSet;
+use problemreductions::models::set::MinimumSetCovering;
+use problemreductions::rules::{ReduceTo, ReductionResult};
+use problemreductions::topology::SimpleGraph;
+use problemreductions::variant::K3;
+use problemreductions::Problem;
+
+#[test]
+fn numeric_boundaries_weight_totals_use_i64() {
+    let dominating =
+        MinimumDominatingSet::new(SimpleGraph::new(2, vec![]), vec![i32::MAX, i32::MAX]);
+    assert_eq!(dominating.evaluate(&[1, 1]).0, Some(4_294_967_294_i64));
+
+    let covering =
+        MinimumSetCovering::with_weights(2, vec![vec![0], vec![1]], vec![i32::MAX, i32::MAX]);
+    assert_eq!(covering.evaluate(&[1, 1]).0, Some(4_294_967_294_i64));
+
+    let ordinary = MinimumSetCovering::with_weights(1, vec![vec![0]], vec![7i32]);
+    assert_eq!(ordinary.evaluate(&[1]).0, Some(7_i64));
+}
+
+#[test]
+fn numeric_boundaries_all_cnf_models_reject_invalid_literals() {
+    for literal in [0, i32::MIN, 2] {
+        let errors = [
+            Satisfiability::try_new(1, vec![CNFClause::new(vec![literal])]).unwrap_err(),
+            KSatisfiability::<K3>::try_new(1, vec![CNFClause::new(vec![literal, 1, 1])])
+                .unwrap_err(),
+            NAESatisfiability::try_new(1, vec![CNFClause::new(vec![literal, 1])]).unwrap_err(),
+            Maximum2Satisfiability::try_new(1, vec![CNFClause::new(vec![literal, 1])]).unwrap_err(),
+            OneInThreeSatisfiability::try_new(1, vec![CNFClause::new(vec![literal, 1, 1])])
+                .unwrap_err(),
+            Planar3Satisfiability::try_new(1, vec![CNFClause::new(vec![literal, 1, 1])])
+                .unwrap_err(),
+            QuantifiedBooleanFormulas::try_new(
+                1,
+                vec![Quantifier::Exists],
+                vec![CNFClause::new(vec![literal])],
+            )
+            .unwrap_err(),
+        ];
+
+        for error in errors {
+            assert!(error.contains(&literal.to_string()), "{error}");
+            assert!(error.contains("1..=1"), "{error}");
+        }
+    }
+}
+
+#[test]
+fn numeric_boundaries_sat_variable_limit_does_not_allocate() {
+    let max = i32::MAX as usize;
+    let formula = Satisfiability::try_new(max, vec![CNFClause::new(vec![i32::MAX])]).unwrap();
+    assert_eq!(formula.num_vars(), max);
+
+    let error = Satisfiability::try_new(max + 1, vec![]).unwrap_err();
+    assert!(error.contains(&(max + 1).to_string()), "{error}");
+    assert!(error.contains(&i32::MAX.to_string()), "{error}");
+}
+
+#[test]
+fn numeric_boundaries_serde_uses_cnf_validation() {
+    let error =
+        serde_json::from_str::<Satisfiability>(r#"{"num_vars":1,"clauses":[{"literals":[0]}]}"#)
+            .unwrap_err()
+            .to_string();
+    assert!(error.contains("invalid literal 0"), "{error}");
+    assert!(error.contains("1..=1"), "{error}");
+}
+
+#[test]
+fn numeric_boundaries_sat_reduction_rejects_exhausted_variable_ids() {
+    let source = Satisfiability::new(i32::MAX as usize, vec![CNFClause::new(vec![i32::MAX])]);
+    let panic = std::panic::catch_unwind(|| {
+        let _ =
+            <Satisfiability as ReduceTo<KSatisfiability<K3>>>::reduce_to(&source).target_problem();
+    })
+    .unwrap_err();
+    let message = panic_message(panic);
+    assert!(
+        message.contains("Satisfiability -> KSatisfiability"),
+        "{message}"
+    );
+    assert!(
+        message.contains("allocate 1 auxiliary variable"),
+        "{message}"
+    );
+    assert!(message.contains(&i32::MAX.to_string()), "{message}");
+}
+
+fn panic_message(panic: Box<dyn std::any::Any + Send>) -> String {
+    if let Some(message) = panic.downcast_ref::<String>() {
+        return message.clone();
+    }
+    panic
+        .downcast_ref::<&str>()
+        .expect("panic payload must be a string")
+        .to_string()
+}

From f7c6f77e35c87a5036006f3cbe9060be2553b82a Mon Sep 17 00:00:00 2001
From: Xiwei Pan <xiwei.pan@connect.hkust-gz.edu.cn>
Date: Fri, 7 Aug 2026 13:20:22 +0800
Subject: [PATCH 2/5] Keep numeric implementation details out of issue
 templates

---
 .claude/CLAUDE.md                         |  5 +++++
 .claude/skills/add-model/SKILL.md         |  3 +--
 .claude/skills/add-rule/SKILL.md          | 13 +++++++------
 .claude/skills/review-structural/SKILL.md |  2 +-
 .github/ISSUE_TEMPLATE/problem.md         | 12 ------------
 .github/ISSUE_TEMPLATE/rule.md            | 12 ------------
 docs/src/design.md                        |  6 ++++--
 7 files changed, 18 insertions(+), 35 deletions(-)

diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index c15470b14..ef69387f1 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -224,6 +224,11 @@ arithmetic is exact or approximate. Use `TryFrom` at range boundaries and
 checked arithmetic for derived values that may overflow. Rust construction,
 serde, CLI, and MCP must enforce the same range.
 
+Issue contributors provide the mathematical definition, domains, and
+constraints; implementers derive the Rust representation. Do not require issue
+authors to choose implementation types or add implementation-specific numeric
+fields to issue templates. Changes to issue templates require user approval.
+
 ### File Naming
 - Reduction files: `src/rules/<source>_<target>.rs` (e.g., `maximumindependentset_qubo.rs`)
 - Model files: `src/models/<category>/<name>.rs` — category is by input structure: `graph/` (graph input), `formula/` (boolean formula/circuit), `set/` (universe + subsets), `algebraic/` (matrix/linear system/lattice), `misc/` (other)
diff --git a/.claude/skills/add-model/SKILL.md b/.claude/skills/add-model/SKILL.md
index 903be1de1..371b747e5 100644
--- a/.claude/skills/add-model/SKILL.md
+++ b/.claude/skills/add-model/SKILL.md
@@ -27,7 +27,6 @@ Before any implementation, collect all required information. If called from `iss
 | 10 | **Solving strategy** | How it can be solved | "BruteForce works; ILP reduction available" |
 | 11 | **Category** | Which sub-module under `src/models/` | `graph`, `formula`, `set`, `algebraic`, `misc` |
 | 12 | **Expected outcome from the issue** | Concrete outcome for the issue's example instance | Objective: one optimal solution + optimal value. Witness: one valid/satisfying solution + why it is valid. Aggregate-only: the final aggregate value and how it is derived |
-| 13 | **Numeric contract** | Every numeric input/domain, computed total type, maximum supported value, checked conversion, overflow behavior, and exact/approximate choice | `weight: i32`, `total: i64`, exact, constructor rejects out-of-range input |
 
 If any item is missing, ask the user to provide it. Do NOT proceed until the checklist is complete.
 
@@ -76,7 +75,7 @@ Read these first to understand the patterns:
 ## Pre-review Checklist
 
 Before implementing, make sure the plan explicitly covers these items that structural review checks later:
-- Numeric choices follow `docs/src/design.md#numeric-types-and-arithmetic`; serde/CLI construction uses the same validation as `new`/`try_new`, and boundary tests cover the declared maximum without requiring impractical allocation
+- Derive numeric implementation types from the mathematical domains in the issue and follow `docs/src/design.md#numeric-types-and-arithmetic`; serde/CLI construction uses the same validation as `new`/`try_new`, and boundary tests cover the supported maximum without requiring impractical allocation
 - `ProblemSchemaEntry` metadata is complete for the current schema shape (`display_name`, `aliases`, `dimensions`, and constructor-facing `fields`)
 - `Problem::Value` uses the correct aggregate wrapper and witness support is intentional
 - `declare_variants!` is present with exactly one `default` variant when multiple concrete variants exist
diff --git a/.claude/skills/add-rule/SKILL.md b/.claude/skills/add-rule/SKILL.md
index 9264a508a..11846e9de 100644
--- a/.claude/skills/add-rule/SKILL.md
+++ b/.claude/skills/add-rule/SKILL.md
@@ -33,7 +33,6 @@ Before any implementation, collect all required information. If called from `iss
 | 7 | **Concrete example** | A small worked-out instance (tutorial style, clear intuition) | "Triangle graph: VC={0,1} -> IS={2}" |
 | 8 | **Solving strategy** | How to solve the target problem | "BruteForce, or existing ILP reduction" |
 | 9 | **Reference** | Paper, textbook, or URL for the reduction | URL or citation |
-| 10 | **Numeric contract** | Source/target numeric fields, totals, size arithmetic, coefficients, bounds, auxiliary IDs, maximum values, checked conversions, overflow behavior, and exact/approximate choice | `usize` source count to checked `i32` SAT IDs |
 
 If any item is missing, ask the user to provide it. Put a high standard on item 7 (concrete example): it must be in tutorial style with clear intuition and easy to understand. Do NOT proceed until the checklist is complete.
 
@@ -59,11 +58,13 @@ If incompatible, STOP and comment on the issue explaining the type mismatch and
 
 ## Numeric Safety Gate
 
-Read `docs/src/design.md#numeric-types-and-arithmetic`. Reject an incomplete
-plan when numeric domains, total types, maxima, or conversions are unspecified.
-Do not use `as` for range/sign changes. Check target-size arithmetic and
-auxiliary identifiers before constructing the target, verify serde/CLI uses the
-same ranges, and add focused tests at the declared boundary.
+Read `docs/src/design.md#numeric-types-and-arithmetic`. Derive implementation
+types, supported ranges, and checked conversions from the mathematical source,
+target, and reduction algorithm. Ask the contributor only when a mathematical
+domain or constraint is ambiguous; do not ask them to choose Rust types. Do not
+use `as` for range/sign changes. Check target-size arithmetic and auxiliary
+identifiers before constructing the target, verify serde/CLI uses the same
+ranges, and add focused boundary tests.
 
 ## Reference Implementations
 
diff --git a/.claude/skills/review-structural/SKILL.md b/.claude/skills/review-structural/SKILL.md
index d32c6b3fb..b22197d7c 100644
--- a/.claude/skills/review-structural/SKILL.md
+++ b/.claude/skills/review-structural/SKILL.md
@@ -66,7 +66,7 @@ Only run if review type includes "model". Given: problem name `P`, category `C`,
 | 14 | Canonical model example registered | `Grep("{P}", "src/example_db/model_builders.rs")` |
 | 15 | Paper `display-name` entry | `Grep('"{P}"', "docs/paper/reductions.typ")` |
 | 16 | Paper `problem-def` block | `Grep('problem-def.*"{P}"', "docs/paper/reductions.typ")` |
-| 17 | Numeric contract | Compare issue fields, schema types, Rust fields, aggregate/total type, constructor and serde validation, conversions, overflow behavior, and boundary tests against `docs/src/design.md#numeric-types-and-arithmetic` |
+| 17 | Numeric contract | Derive the expected representation from the mathematical definition, then compare schema types, Rust fields, aggregate/total type, constructor and serde validation, conversions, overflow behavior, and boundary tests against `docs/src/design.md#numeric-types-and-arithmetic` |
 
 ### Rule Checklist
 
diff --git a/.github/ISSUE_TEMPLATE/problem.md b/.github/ISSUE_TEMPLATE/problem.md
index e5214d071..412397888 100644
--- a/.github/ISSUE_TEMPLATE/problem.md
+++ b/.github/ISSUE_TEMPLATE/problem.md
@@ -50,18 +50,6 @@ Connect fields to the symbols defined above.
 | <!-- e.g. graph --> | <!-- e.g. SimpleGraph --> | <!-- e.g. the graph G=(V,E) --> |
 | <!-- e.g. weights --> | <!-- e.g. list of W --> | <!-- e.g. vertex weights w_i for each i ∈ V (weighted variant only) --> |
 
-## Numeric Contract
-
-<!-- Follow docs/src/design.md#numeric-types-and-arithmetic. Distinguish the
-type of one input value from the type of a sum or product. -->
-
-| Quantity | Meaning and domain | Input type | Computed/total type | Maximum supported value | Checked conversions |
-|----------|--------------------|------------|---------------------|-------------------------|---------------------|
-| <!-- e.g. w_i --> | <!-- signed vertex weight --> | <!-- i32 --> | <!-- i64 total --> | <!-- i64::MAX total --> | <!-- i32 -> i64 via From --> |
-
-- **Overflow behavior:** <!-- What construction rejects and what error is reported -->
-- **Arithmetic:** <!-- Exact integer, or approximate f64 with justification -->
-
 ## Complexity
 
 - **Best known exact algorithm:** <!-- e.g. O(1.1996^n) by Xiao & Nagamochi (2017), where n = |V| -->
diff --git a/.github/ISSUE_TEMPLATE/rule.md b/.github/ISSUE_TEMPLATE/rule.md
index ca49e2dd2..230db8452 100644
--- a/.github/ISSUE_TEMPLATE/rule.md
+++ b/.github/ISSUE_TEMPLATE/rule.md
@@ -45,18 +45,6 @@ Use the symbols defined in the Reduction Algorithm above. -->
 | <!-- e.g. number of variables --> | <!-- e.g. n = |V| --> |
 | <!-- e.g. number of edges --> | <!-- e.g. m = |E| --> |
 
-## Numeric Contract
-
-<!-- Follow docs/src/design.md#numeric-types-and-arithmetic. Include source and
-target values, size calculations, coefficients, bounds, and auxiliary IDs. -->
-
-| Quantity | Meaning and domain | Source type | Target/computed type | Maximum supported value | Checked conversions |
-|----------|--------------------|-------------|----------------------|-------------------------|---------------------|
-| <!-- e.g. auxiliary variable --> | <!-- positive SAT variable ID --> | <!-- usize count --> | <!-- i32 literal --> | <!-- i32::MAX --> | <!-- i32::try_from --> |
-
-- **Overflow behavior:** <!-- Where the reduction stops and what error is reported -->
-- **Arithmetic:** <!-- Exact integer, or approximate f64 with justification -->
-
 ## Validation Method
 
 <!-- How to verify the reduction is correct beyond closed-loop testing?
diff --git a/docs/src/design.md b/docs/src/design.md
index fcbbf90b3..9e56a4df6 100644
--- a/docs/src/design.md
+++ b/docs/src/design.md
@@ -124,9 +124,11 @@ An integer-to-floating conversion is permitted only at an explicitly
 approximate solver boundary, where the exactly representable input range and
 out-of-range behavior are documented.
 
-### Numeric review checklist
+### Numeric implementation review checklist
 
-For every new model or reduction, record:
+Issue authors describe mathematical objects, domains, and constraints; they are
+not expected to choose Rust types. During implementation and review, derive and
+record:
 
 1. every numeric input, its meaning, and its mathematical domain;
 2. every computed total/product and its result type;

From bc772f555d161059c139d936ed8eebc17e0235e2 Mon Sep 17 00:00:00 2001
From: Xiwei Pan <xiwei.pan@connect.hkust-gz.edu.cn>
Date: Fri, 7 Aug 2026 13:50:54 +0800
Subject: [PATCH 3/5] Move SAT allocation into rule helpers

---
 src/models/formula/mod.rs                     |  1 -
 src/models/formula/sat.rs                     | 63 ------------------
 src/rules/circuit_sat.rs                      |  3 +-
 ...satisfiability_oneinthreesatisfiability.rs |  5 +-
 src/rules/ksatisfiability_timetabledesign.rs  |  3 +-
 src/rules/mod.rs                              |  1 +
 src/rules/sat_helpers.rs                      | 66 +++++++++++++++++++
 src/rules/sat_ksat.rs                         |  3 +-
 .../satisfiability_maximum2satisfiability.rs  |  5 +-
 src/rules/satisfiability_naesatisfiability.rs |  3 +-
 src/unit_tests/models/formula/sat.rs          | 27 --------
 src/unit_tests/rules/sat_helpers.rs           | 28 ++++++++
 12 files changed, 107 insertions(+), 101 deletions(-)
 create mode 100644 src/rules/sat_helpers.rs
 create mode 100644 src/unit_tests/rules/sat_helpers.rs

diff --git a/src/models/formula/mod.rs b/src/models/formula/mod.rs
index 6b4fe0725..e2c09d8d8 100644
--- a/src/models/formula/mod.rs
+++ b/src/models/formula/mod.rs
@@ -29,7 +29,6 @@ pub use non_tautology::NonTautology;
 pub use one_in_three_satisfiability::OneInThreeSatisfiability;
 pub use planar_3_satisfiability::Planar3Satisfiability;
 pub use qbf::{QuantifiedBooleanFormulas, Quantifier};
-pub(crate) use sat::SatVariableAllocator;
 pub use sat::{CNFClause, Satisfiability};
 
 /// Convert a binary config (0/1 per variable) to a boolean assignment.
diff --git a/src/models/formula/sat.rs b/src/models/formula/sat.rs
index 0cc5a44ca..0557598a2 100644
--- a/src/models/formula/sat.rs
+++ b/src/models/formula/sat.rs
@@ -255,69 +255,6 @@ pub(super) fn validate_cnf_literals(num_vars: usize, clauses: &[CNFClause]) -> R
     Ok(())
 }
 
-#[derive(Debug)]
-pub(crate) struct SatVariableAllocator {
-    reduction: &'static str,
-    next: u64,
-}
-
-impl SatVariableAllocator {
-    pub(crate) fn new(reduction: &'static str, existing: usize) -> Result<Self, String> {
-        if existing > i32::MAX as usize {
-            return Err(format!(
-                "{reduction} has {existing} source variables; SAT variable numbers are limited to {}",
-                i32::MAX
-            ));
-        }
-        Ok(Self {
-            reduction,
-            next: u64::try_from(existing).expect("usize SAT count fits u64") + 1,
-        })
-    }
-
-    pub(crate) fn allocate(&mut self) -> Result<i32, String> {
-        let variable = self.next;
-        if variable > i32::MAX as u64 {
-            return Err(format!(
-                "{} cannot allocate 1 auxiliary variable after {}; SAT variable numbers are limited to {}",
-                self.reduction,
-                self.num_vars(),
-                i32::MAX
-            ));
-        }
-        self.next += 1;
-        Ok(i32::try_from(variable).expect("checked SAT variable fits i32"))
-    }
-
-    pub(crate) fn allocate_many(&mut self, count: usize) -> Result<Vec<i32>, String> {
-        if count == 0 {
-            return Ok(Vec::new());
-        }
-        let count = u64::try_from(count).expect("usize allocation count fits u64");
-        let last = self
-            .next
-            .checked_add(count - 1)
-            .ok_or_else(|| format!("{} auxiliary variable count overflow", self.reduction))?;
-        if last > i32::MAX as u64 {
-            return Err(format!(
-                "{} cannot allocate {count} auxiliary variables after {}; SAT variable numbers are limited to {}",
-                self.reduction,
-                self.num_vars(),
-                i32::MAX
-            ));
-        }
-        let variables = (self.next..=last)
-            .map(|variable| i32::try_from(variable).expect("checked SAT variable fits i32"))
-            .collect();
-        self.next = last + 1;
-        Ok(variables)
-    }
-
-    pub(crate) fn num_vars(&self) -> usize {
-        usize::try_from(self.next - 1).expect("SAT variable count fits usize")
-    }
-}
-
 /// Check if an assignment satisfies a SAT formula.
 ///
 /// # Arguments
diff --git a/src/rules/circuit_sat.rs b/src/rules/circuit_sat.rs
index 4f9549caa..7154dd170 100644
--- a/src/rules/circuit_sat.rs
+++ b/src/rules/circuit_sat.rs
@@ -1,9 +1,10 @@
 //! Reduction from CircuitSAT to Satisfiability via Tseitin encoding.
 
 use crate::models::formula::{
-    Assignment, BooleanExpr, BooleanOp, CNFClause, CircuitSAT, SatVariableAllocator, Satisfiability,
+    Assignment, BooleanExpr, BooleanOp, CNFClause, CircuitSAT, Satisfiability,
 };
 use crate::reduction;
+use crate::rules::sat_helpers::SatVariableAllocator;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 use std::collections::HashMap;
 
diff --git a/src/rules/ksatisfiability_oneinthreesatisfiability.rs b/src/rules/ksatisfiability_oneinthreesatisfiability.rs
index f84b3abbb..7d19e7fab 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.
 
-use crate::models::formula::{
-    CNFClause, KSatisfiability, OneInThreeSatisfiability, SatVariableAllocator,
-};
+use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability};
 use crate::reduction;
+use crate::rules::sat_helpers::SatVariableAllocator;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 use crate::variant::K3;
 
diff --git a/src/rules/ksatisfiability_timetabledesign.rs b/src/rules/ksatisfiability_timetabledesign.rs
index cb02c5f97..69016f132 100644
--- a/src/rules/ksatisfiability_timetabledesign.rs
+++ b/src/rules/ksatisfiability_timetabledesign.rs
@@ -20,9 +20,10 @@
 //! graph; the colors on the two special variable edges recover the satisfying
 //! truth assignment.
 
-use crate::models::formula::{CNFClause, KSatisfiability, SatVariableAllocator};
+use crate::models::formula::{CNFClause, KSatisfiability};
 use crate::models::misc::TimetableDesign;
 use crate::reduction;
+use crate::rules::sat_helpers::SatVariableAllocator;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 #[cfg(any(test, feature = "example-db"))]
 use crate::traits::Problem;
diff --git a/src/rules/mod.rs b/src/rules/mod.rs
index b6ed58db3..52a01e202 100644
--- a/src/rules/mod.rs
+++ b/src/rules/mod.rs
@@ -130,6 +130,7 @@ pub(crate) mod prizecollectingsteinerforest_steinertree;
 pub(crate) mod rootedtreearrangement_rootedtreestorageassignment;
 pub(crate) mod sat_circuitsat;
 pub(crate) mod sat_coloring;
+pub(crate) mod sat_helpers;
 pub(crate) mod sat_ksat;
 pub(crate) mod sat_maximumindependentset;
 pub(crate) mod sat_minimumdominatingset;
diff --git a/src/rules/sat_helpers.rs b/src/rules/sat_helpers.rs
new file mode 100644
index 000000000..83d838735
--- /dev/null
+++ b/src/rules/sat_helpers.rs
@@ -0,0 +1,66 @@
+#[derive(Debug)]
+pub(crate) struct SatVariableAllocator {
+    reduction: &'static str,
+    next: u64,
+}
+
+impl SatVariableAllocator {
+    pub(crate) fn new(reduction: &'static str, existing: usize) -> Result<Self, String> {
+        if existing > i32::MAX as usize {
+            return Err(format!(
+                "{reduction} has {existing} source variables; SAT variable numbers are limited to {}",
+                i32::MAX
+            ));
+        }
+        Ok(Self {
+            reduction,
+            next: u64::try_from(existing).expect("usize SAT count fits u64") + 1,
+        })
+    }
+
+    pub(crate) fn allocate(&mut self) -> Result<i32, String> {
+        let variable = self.next;
+        if variable > i32::MAX as u64 {
+            return Err(format!(
+                "{} cannot allocate 1 auxiliary variable after {}; SAT variable numbers are limited to {}",
+                self.reduction,
+                self.num_vars(),
+                i32::MAX
+            ));
+        }
+        self.next += 1;
+        Ok(i32::try_from(variable).expect("checked SAT variable fits i32"))
+    }
+
+    pub(crate) fn allocate_many(&mut self, count: usize) -> Result<Vec<i32>, String> {
+        if count == 0 {
+            return Ok(Vec::new());
+        }
+        let count = u64::try_from(count).expect("usize allocation count fits u64");
+        let last = self
+            .next
+            .checked_add(count - 1)
+            .ok_or_else(|| format!("{} auxiliary variable count overflow", self.reduction))?;
+        if last > i32::MAX as u64 {
+            return Err(format!(
+                "{} cannot allocate {count} auxiliary variables after {}; SAT variable numbers are limited to {}",
+                self.reduction,
+                self.num_vars(),
+                i32::MAX
+            ));
+        }
+        let variables = (self.next..=last)
+            .map(|variable| i32::try_from(variable).expect("checked SAT variable fits i32"))
+            .collect();
+        self.next = last + 1;
+        Ok(variables)
+    }
+
+    pub(crate) fn num_vars(&self) -> usize {
+        usize::try_from(self.next - 1).expect("SAT variable count fits usize")
+    }
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/sat_helpers.rs"]
+mod tests;
diff --git a/src/rules/sat_ksat.rs b/src/rules/sat_ksat.rs
index a72036704..6823d263f 100644
--- a/src/rules/sat_ksat.rs
+++ b/src/rules/sat_ksat.rs
@@ -6,8 +6,9 @@
 //!
 //! K-SAT -> SAT: Trivial embedding (K-SAT is a special case of SAT)
 
-use crate::models::formula::{CNFClause, KSatisfiability, SatVariableAllocator, Satisfiability};
+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};
 
diff --git a/src/rules/satisfiability_maximum2satisfiability.rs b/src/rules/satisfiability_maximum2satisfiability.rs
index c245ac17f..e5cb5a667 100644
--- a/src/rules/satisfiability_maximum2satisfiability.rs
+++ b/src/rules/satisfiability_maximum2satisfiability.rs
@@ -1,9 +1,8 @@
 //! Reduction from Satisfiability to Maximum 2-Satisfiability.
 
-use crate::models::formula::{
-    CNFClause, Maximum2Satisfiability, SatVariableAllocator, Satisfiability,
-};
+use crate::models::formula::{CNFClause, Maximum2Satisfiability, Satisfiability};
 use crate::reduction;
+use crate::rules::sat_helpers::SatVariableAllocator;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 
 /// Result of reducing SAT to MAX-2-SAT.
diff --git a/src/rules/satisfiability_naesatisfiability.rs b/src/rules/satisfiability_naesatisfiability.rs
index 39a777bd5..66a7ba122 100644
--- a/src/rules/satisfiability_naesatisfiability.rs
+++ b/src/rules/satisfiability_naesatisfiability.rs
@@ -7,8 +7,9 @@
 //! has at least one false literal (the sentinel itself when s=false, or
 //! the complement of the original satisfied literal when s=true).
 
-use crate::models::formula::{CNFClause, NAESatisfiability, SatVariableAllocator, Satisfiability};
+use crate::models::formula::{CNFClause, NAESatisfiability, Satisfiability};
 use crate::reduction;
+use crate::rules::sat_helpers::SatVariableAllocator;
 use crate::rules::traits::{ReduceTo, ReductionResult};
 
 /// Result of reducing Satisfiability to NAE-Satisfiability.
diff --git a/src/unit_tests/models/formula/sat.rs b/src/unit_tests/models/formula/sat.rs
index 392a282ba..54573115c 100644
--- a/src/unit_tests/models/formula/sat.rs
+++ b/src/unit_tests/models/formula/sat.rs
@@ -3,33 +3,6 @@ use crate::solvers::BruteForce;
 use crate::traits::Problem;
 include!("../../jl_helpers.rs");
 
-#[test]
-fn test_sat_variable_allocator_numeric_boundaries() {
-    let mut allocator = SatVariableAllocator::new("test reduction", i32::MAX as usize - 1)
-        .expect("largest valid starting count");
-    assert_eq!(allocator.allocate().unwrap(), i32::MAX);
-    assert_eq!(allocator.num_vars(), i32::MAX as usize);
-
-    let error = allocator.allocate().unwrap_err();
-    assert!(error.contains("test reduction"));
-    assert!(error.contains("limited to 2147483647"));
-}
-
-#[test]
-fn test_sat_variable_allocator_batch_numeric_boundaries() {
-    let mut exact = SatVariableAllocator::new("exact batch", i32::MAX as usize - 2).unwrap();
-    assert_eq!(
-        exact.allocate_many(2).unwrap(),
-        vec![i32::MAX - 1, i32::MAX]
-    );
-    assert_eq!(exact.num_vars(), i32::MAX as usize);
-
-    let mut overflow = SatVariableAllocator::new("overflow batch", i32::MAX as usize - 1).unwrap();
-    let error = overflow.allocate_many(2).unwrap_err();
-    assert!(error.contains("cannot allocate 2 auxiliary variables"));
-    assert_eq!(overflow.num_vars(), i32::MAX as usize - 1);
-}
-
 #[test]
 fn test_cnf_clause_creation() {
     let clause = CNFClause::new(vec![1, -2, 3]);
diff --git a/src/unit_tests/rules/sat_helpers.rs b/src/unit_tests/rules/sat_helpers.rs
new file mode 100644
index 000000000..45f8b610d
--- /dev/null
+++ b/src/unit_tests/rules/sat_helpers.rs
@@ -0,0 +1,28 @@
+use super::*;
+
+#[test]
+fn test_sat_variable_allocator_numeric_boundaries() {
+    let mut allocator = SatVariableAllocator::new("test reduction", i32::MAX as usize - 1)
+        .expect("largest valid starting count");
+    assert_eq!(allocator.allocate().unwrap(), i32::MAX);
+    assert_eq!(allocator.num_vars(), i32::MAX as usize);
+
+    let error = allocator.allocate().unwrap_err();
+    assert!(error.contains("test reduction"));
+    assert!(error.contains("limited to 2147483647"));
+}
+
+#[test]
+fn test_sat_variable_allocator_batch_numeric_boundaries() {
+    let mut exact = SatVariableAllocator::new("exact batch", i32::MAX as usize - 2).unwrap();
+    assert_eq!(
+        exact.allocate_many(2).unwrap(),
+        vec![i32::MAX - 1, i32::MAX]
+    );
+    assert_eq!(exact.num_vars(), i32::MAX as usize);
+
+    let mut overflow = SatVariableAllocator::new("overflow batch", i32::MAX as usize - 1).unwrap();
+    let error = overflow.allocate_many(2).unwrap_err();
+    assert!(error.contains("cannot allocate 2 auxiliary variables"));
+    assert_eq!(overflow.num_vars(), i32::MAX as usize - 1);
+}

From a25af77abb24f494b03c4b1c8f3190e6ddc3feba Mon Sep 17 00:00:00 2001
From: Xiwei Pan <xiwei.pan@connect.hkust-gz.edu.cn>
Date: Fri, 7 Aug 2026 14:13:37 +0800
Subject: [PATCH 4/5] Tighten structural semantic review

---
 .claude/skills/review-structural/SKILL.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.claude/skills/review-structural/SKILL.md b/.claude/skills/review-structural/SKILL.md
index b22197d7c..a22152eb3 100644
--- a/.claude/skills/review-structural/SKILL.md
+++ b/.claude/skills/review-structural/SKILL.md
@@ -108,6 +108,8 @@ Report pass/fail. If tests fail, identify which tests. **Do NOT fix anything** 
 
 ## Step 4: Semantic Review
 
+For both review types, verify that changed mathematical comments state exactly what the code proves and that changed failure messages name the actual rejected quantity and remain meaningful at zero and boundary values.
+
 ### For Models:
 1. **`evaluate()` correctness** — Does it check feasibility before computing the objective when the model has invalid configurations? Objective models should return `Max/Min/Extremum(None)` for infeasible configs, witness problems should return `false`, and aggregate-only models should return the per-configuration contribution that matches the intended fold semantics.
 2. **`dims()` correctness** — Does it return the actual configuration space? (e.g., `vec![2; n]` for binary)

From 2ff9fabe8088a56b04f00ac5bd6c7e0813a87e58 Mon Sep 17 00:00:00 2001
From: Xiwei Pan <xiwei.pan@connect.hkust-gz.edu.cn>
Date: Fri, 7 Aug 2026 14:16:13 +0800
Subject: [PATCH 5/5] Revert structural review wording

---
 .claude/skills/review-structural/SKILL.md | 2 --
 1 file changed, 2 deletions(-)

diff --git a/.claude/skills/review-structural/SKILL.md b/.claude/skills/review-structural/SKILL.md
index a22152eb3..b22197d7c 100644
--- a/.claude/skills/review-structural/SKILL.md
+++ b/.claude/skills/review-structural/SKILL.md
@@ -108,8 +108,6 @@ Report pass/fail. If tests fail, identify which tests. **Do NOT fix anything** 
 
 ## Step 4: Semantic Review
 
-For both review types, verify that changed mathematical comments state exactly what the code proves and that changed failure messages name the actual rejected quantity and remain meaningful at zero and boundary values.
-
 ### For Models:
 1. **`evaluate()` correctness** — Does it check feasibility before computing the objective when the model has invalid configurations? Objective models should return `Max/Min/Extremum(None)` for infeasible configs, witness problems should return `false`, and aggregate-only models should return the per-configuration contribution that matches the intended fold semantics.
 2. **`dims()` correctness** — Does it return the actual configuration space? (e.g., `vec![2; n]` for binary)