Establish numeric types and arithmetic standard

[isPANN]

Stacked on #1083 and targets 1075-growth-domain.

Closes #1116

Summary

• establish the repository numeric type and arithmetic contract in design docs and implementation/review guidance
• keep issue templates mathematical and free of implementation-specific numeric fields
• widen integral weight accumulation and decision bounds to i64, including CLI schema exposure
• centralize CNF literal validation across construction and deserialization
• add a checked SAT variable allocator and migrate SAT-producing reductions to it
• add focused overflow, literal-boundary, serde, and allocator-exhaustion regressions

No tests were deleted.

Verification

• cargo fmt --all
• git diff --check
• make clippy
• make test
• make doc

[Copilot]

Pull request overview

This PR establishes and applies a repository-wide numeric-types/arithmetic contract (including overflow and conversion rules), migrates weight totals and decision bounds to i64, and standardizes SAT CNF literal validation plus auxiliary-variable allocation to prevent underflow/overflow and inconsistent SAT handling across constructors, serde, and reductions.

Changes:

• Document numeric type/overflow/conversion rules in contributor-facing docs and templates; add numeric-review checklist guidance.
• Widen exact integer accumulations and decision bounds to i64 (including CLI schema exposure) and update affected models/reductions/unit tests.
• Centralize CNF literal validation across constructors and serde, add a checked SAT variable allocator, migrate SAT-producing reductions, and add boundary regression tests.

Reviewed changes

Copilot reviewed 54 out of 54 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
tests/suites/numeric_boundaries.rs	New regression suite covering i64 weight totals, CNF literal validation, serde validation, and SAT allocator exhaustion.
tests/main.rs	Registers the new numeric boundaries suite.
src/unit_tests/rules/sat_ksat.rs	Updates K-SAT structural test to reflect correct source variable count.
src/unit_tests/rules/minimumvertexcover_comparativecontainment.rs	Updates decision-bound helper signature to i64.
src/unit_tests/rules/maximum2satisfiability_maxcut.rs	Replaces unchecked cast with checked i64 conversion.
src/unit_tests/rules/maxcut_minimummatrixcover.rs	Removes unnecessary cast after widening cut totals.
src/unit_tests/rules/hamiltoniancircuit_ruralpostman.rs	Uses checked usize -> i64 conversion in derived bound arithmetic.
src/unit_tests/rules/exactcoverby3sets_boundeddiameterspanningtree.rs	Uses checked arithmetic and checked i64 conversion for derived bounds.
src/unit_tests/rules/decisionminimumvertexcover_hamiltoniancircuit.rs	Updates decision bound type to i64.
src/unit_tests/rules/decisionminimumdominatingset_minmaxmulticenter.rs	Updates decision bound type to i64.
src/unit_tests/rules/decisionminimumdominatingset_minimumsummulticenter.rs	Updates decision bound type to i64 and makes derived arithmetic checked.
src/unit_tests/models/set/minimum_set_covering.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/set/maximum_set_packing.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/graph/spin_glass.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/graph/minimum_vertex_cover.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/graph/minimum_dominating_set.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/graph/maximum_matching.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/graph/maximum_independent_set.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/graph/maximal_is.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/graph/max_cut.rs	Aligns JL parity test comparisons with widened totals.
src/unit_tests/models/formula/sat.rs	Adds SAT allocator boundary tests and updates zero-var UNSAT case to use an empty clause.
src/unit_tests/models/formula/qbf.rs	Updates zero-var UNSAT case to avoid invalid literals under stricter validation.
src/unit_tests/models/formula/planar_3_satisfiability.rs	Updates expected panic text to match standardized CNF literal error messages.
src/unit_tests/models/formula/one_in_three_satisfiability.rs	Updates expected panic text to match standardized CNF literal error messages.
src/types.rs	Changes WeightElement accumulation for i32 and One to i64 totals; updates docs/comments accordingly.
src/solvers/decision_search.rs	Widens decision-search bounds and optimization inner types from i32 to i64.
src/rules/satisfiability_naesatisfiability.rs	Migrates sentinel variable creation to checked SAT allocator.
src/rules/satisfiability_maximum2satisfiability.rs	Uses SAT allocator for auxiliary IDs and adds checked capacity arithmetic.
src/rules/sat_ksat.rs	Uses SAT allocator for auxiliary IDs and makes clause normalization allocation checked.
src/rules/minimumvertexcover_comparativecontainment.rs	Updates trivial-bound handling for widened decision bounds.
src/rules/ksatisfiability_timetabledesign.rs	Uses allocator for new SAT vars and replaces unchecked casts with checked conversions.
src/rules/ksatisfiability_oneinthreesatisfiability.rs	Uses allocator for auxiliary IDs and adds checked capacity arithmetic.
src/rules/ksatisfiability_decisionminimumvertexcover.rs	Computes decision bound with checked arithmetic and widens to i64.
src/rules/ksatisfiability_acyclicpartition.rs	Widens bounds to i64 and removes now-obsolete helper conversion.
src/rules/hamiltoniancircuit_strongconnectivityaugmentation.rs	Widens derived budget/bound to i64 with checked conversion.
src/rules/hamiltoniancircuit_biconnectivityaugmentation.rs	Widens derived budget/bound to i64 with checked conversion.
src/rules/exactcoverby3sets_boundeddiameterspanningtree.rs	Widens derived weight bound to i64 with checked arithmetic.
src/rules/circuit_sat.rs	Uses checked SAT allocator for Tseitin IDs rather than unchecked increments/casts.
src/models/graph/mixed_chinese_postman.rs	Updates weight-total type bounds to i64-accumulating weights and removes redundant casts.
src/models/formula/sat.rs	Centralizes CNF literal validation (constructor + serde) and introduces SAT variable allocator.
src/models/formula/qbf.rs	Applies the same CNF literal validation contract via try_new and serde try_from.
src/models/formula/planar_3_satisfiability.rs	Moves clause validation to try_new and shares CNF literal validation with SAT.
src/models/formula/one_in_three_satisfiability.rs	Moves clause validation to try_new and shares CNF literal validation with SAT.
src/models/formula/nae_satisfiability.rs	Ensures NAE-SAT construction shares CNF literal validation before width checks.
src/models/formula/mod.rs	Re-exports allocator for internal reduction use.
src/models/formula/maximum_2_satisfiability.rs	Moves clause validation to try_new and shares CNF literal validation with SAT.
src/models/formula/ksat.rs	Implements custom Deserialize to route through try_new and shared CNF literal validation.
problemreductions-cli/src/commands/create/schema_support.rs	Updates schema-derived W::Sum type mapping (i32/One → i64).
problemreductions-cli/src/commands/create.rs	Widens CLI decision bound plumbing for Decision MVC creation to i64.
docs/src/design.md	Adds numeric types/arithmetic standard (domains, ranges, conversions, overflow rules, SAT encoding rules, checklist).
.github/ISSUE_TEMPLATE/rule.md	Adds a Numeric Contract section to rule issue template.
.github/ISSUE_TEMPLATE/problem.md	Adds a Numeric Contract section to problem issue template.
.claude/skills/review-structural/SKILL.md	Adds numeric contract checks to structural review guidance.
.claude/skills/add-rule/SKILL.md	Adds numeric safety gate and numeric contract requirements for new rules.
.claude/skills/add-model/SKILL.md	Adds numeric contract requirements for new models.
.claude/CLAUDE.md	Adds repo-wide numeric contract guidance for contributors/reviewers.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.