Establish numeric types and arithmetic standard

.claude/CLAUDE.md

@@ -214,6 +214,21 @@ 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.
+
+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)

.claude/skills/add-model/SKILL.md

@@ -75,6 +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:
+- 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

.claude/skills/add-rule/SKILL.md

@@ -56,6 +56,16 @@ 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`. 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
 
 Read these first to understand the patterns:

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

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,95 @@ 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 implementation review checklist
+
+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;
+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.

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" => {

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",
     }

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.