diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 502e837f5..ef69387f1 100644 --- a/.claude/CLAUDE.md +++ b/.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/_.rs` (e.g., `maximumindependentset_qubo.rs`) - Model files: `src/models//.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..371b747e5 100644 --- a/.claude/skills/add-model/SKILL.md +++ b/.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 diff --git a/.claude/skills/add-rule/SKILL.md b/.claude/skills/add-rule/SKILL.md index 5e9b01ea6..11846e9de 100644 --- a/.claude/skills/add-rule/SKILL.md +++ b/.claude/skills/add-rule/SKILL.md @@ -56,6 +56,16 @@ grep "type Value = " src/models/*/.rs src/models/*/.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: diff --git a/.claude/skills/review-structural/SKILL.md b/.claude/skills/review-structural/SKILL.md index cdf144284..b22197d7c 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 | 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 diff --git a/docs/src/design.md b/docs/src/design.md index 20f351018..9e56a4df6 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 @@ -45,6 +48,95 @@ trait Problem: Clone { - **Aggregate-only problems** — use fold values such as `Sum` or `And`; these solve to a value but do not admit representative witness configurations. - **Common aggregate wrappers** — `Max`, `Min`, `Sum`, `Or`, `And`, `Extremum`, `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>` 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. 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, - bound: i32, + bound: i64, ) -> Result { 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 { 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 { /// Number of variables. num_vars: usize, @@ -104,6 +103,22 @@ pub struct KSatisfiability { _phantom: std::marker::PhantomData, } +#[derive(Deserialize)] +struct KSatisfiabilityDef { + num_vars: usize, + clauses: Vec, +} + +impl<'de, K: KValue> Deserialize<'de> for KSatisfiability { + fn deserialize(deserializer: D) -> Result + where + D: Deserializer<'de>, + { + let value = KSatisfiabilityDef::deserialize(deserializer)?; + Self::try_new(value.num_vars, value.clauses).map_err(D::Error::custom) + } +} + impl KSatisfiability { /// Create a new K-SAT problem. /// @@ -112,22 +127,27 @@ impl KSatisfiability { /// concrete value like K2, K3). When K is KN (arbitrary), no clause-length /// validation is performed. pub fn new(num_vars: usize, clauses: Vec) -> 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) -> Result { + 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 KSatisfiability { /// 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) -> 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) -> Result { + 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) -> 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) -> Result { + 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, +} + +impl TryFrom for Maximum2Satisfiability { + type Error = String; + + fn try_from(value: Maximum2SatisfiabilityDef) -> Result { + Self::try_new(value.num_vars, value.clauses) + } +} + #[cfg(feature = "example-db")] pub(crate) fn canonical_model_example_specs() -> Vec { vec![crate::example_db::specs::ModelExampleSpec { 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) -> Result { + 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) -> 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) -> Result { + 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, +} + +impl TryFrom for OneInThreeSatisfiability { + type Error = String; + + fn try_from(value: OneInThreeSatisfiabilityDef) -> Result { + Self::try_new(value.num_vars, value.clauses) + } +} + #[cfg(feature = "example-db")] pub(crate) fn canonical_model_example_specs() -> Vec { 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) -> 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) -> Result { + 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, +} + +impl TryFrom for Planar3Satisfiability { + type Error = String; + + fn try_from(value: Planar3SatisfiabilityDef) -> Result { + Self::try_new(value.num_vars, value.clauses) + } +} + #[cfg(feature = "example-db")] pub(crate) fn canonical_model_example_specs() -> Vec { 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, clauses: Vec) -> 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, + clauses: Vec, + ) -> Result { + 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, + clauses: Vec, +} + +impl TryFrom for QuantifiedBooleanFormulas { + type Error = String; + + fn try_from(value: QuantifiedBooleanFormulasDef) -> Result { + Self::try_new(value.num_vars, value.quantifiers, value.clauses) + } +} + #[cfg(feature = "example-db")] pub(crate) fn canonical_model_example_specs() -> Vec { vec![crate::example_db::specs::ModelExampleSpec { diff --git a/src/models/formula/sat.rs b/src/models/formula/sat.rs index 8be2e2b90..0557598a2 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 { 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) -> 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) -> Result { + validate_cnf_literals(num_vars, &clauses)?; + Ok(Self { num_vars, clauses }) } /// Get the number of variables. @@ -197,6 +212,49 @@ crate::declare_variants! { default Satisfiability => "2^num_variables", } +#[derive(Deserialize)] +struct SatisfiabilityDef { + num_vars: usize, + clauses: Vec, +} + +impl TryFrom for Satisfiability { + type Error = String; + + fn try_from(value: SatisfiabilityDef) -> Result { + 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(()) +} + /// 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> { +pub struct MixedChinesePostman> { graph: MixedGraph, arc_weights: Vec, edge_weights: Vec, } -impl> MixedChinesePostman { +impl> MixedChinesePostman { /// Create a new mixed Chinese postman instance. /// /// # Panics @@ -157,11 +157,11 @@ impl> MixedChinesePostman { .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> MixedChinesePostman { fn base_cost(&self) -> i64 { self.arc_weights .iter() - .map(|weight| i64::from(weight.to_sum())) + .map(WeightElement::to_sum) .sum::() + self .edge_weights .iter() - .map(|weight| i64::from(weight.to_sum())) + .map(WeightElement::to_sum) .sum::() } } impl MixedChinesePostman where - W: WeightElement + crate::variant::VariantParam, + W: WeightElement + crate::variant::VariantParam, { /// Check whether a configuration yields a valid orientation (strongly /// connected with proper coverage). @@ -195,7 +195,7 @@ where impl Problem for MixedChinesePostman where - W: WeightElement + crate::variant::VariantParam, + W: WeightElement + crate::variant::VariantParam, { const NAME: &'static str = "MixedChinesePostman"; type Value = Min; @@ -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..7154dd170 100644 --- a/src/rules/circuit_sat.rs +++ b/src/rules/circuit_sat.rs @@ -4,6 +4,7 @@ use crate::models::formula::{ 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; @@ -33,21 +34,26 @@ struct TseitinEncoding { struct TseitinEncoder { source_var_ids: HashMap, clauses: Vec, - 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 +63,7 @@ impl TseitinEncoder { } TseitinEncoding { - num_vars: (self.next_var - 1) as usize, + num_vars: self.variables.num_vars(), clauses: self.clauses, } } @@ -152,9 +158,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> 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> 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> for 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>> for KSatisfiabilit let base_reduction = as ReduceTo< MinimumVertexCover, >>::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..7d19e7fab 100644 --- a/src/rules/ksatisfiability_oneinthreesatisfiability.rs +++ b/src/rules/ksatisfiability_oneinthreesatisfiability.rs @@ -2,6 +2,7 @@ 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; @@ -38,33 +39,44 @@ impl ReduceTo for KSatisfiability { 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..69016f132 100644 --- a/src/rules/ksatisfiability_timetabledesign.rs +++ b/src/rules/ksatisfiability_timetabledesign.rs @@ -23,6 +23,7 @@ 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; @@ -128,7 +129,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 +204,11 @@ fn normalize_formula(source: &KSatisfiability) -> 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 +225,38 @@ fn normalize_formula(source: &KSatisfiability) -> 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 = (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 +264,16 @@ fn normalize_formula(source: &KSatisfiability) -> 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> for Decision= 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/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 { + 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 { + 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, 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 2bf711699..6823d263f 100644 --- a/src/rules/sat_ksat.rs +++ b/src/rules/sat_ksat.rs @@ -8,6 +8,7 @@ use crate::models::formula::{CNFClause, KSatisfiability, Satisfiability}; use crate::reduction; +use crate::rules::sat_helpers::SatVariableAllocator; use crate::rules::traits::{ReduceTo, ReductionResult}; use crate::variant::{KValue, K2, K3, KN}; @@ -55,16 +56,12 @@ impl ReductionResult for ReductionSATToKSAT { /// * `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, - mut next_var: i32, -) -> i32 { + variables: &mut SatVariableAllocator, +) -> Result<(), String> { let len = clause.len(); if len == k { @@ -74,25 +71,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 = clause.literals[..k - 1].to_vec(); @@ -105,10 +100,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 +123,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..e5cb5a667 100644 --- a/src/rules/satisfiability_maximum2satisfiability.rs +++ b/src/rules/satisfiability_maximum2satisfiability.rs @@ -2,6 +2,7 @@ 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. @@ -29,19 +30,22 @@ impl ReductionResult for ReductionSatisfiabilityToMaximum2Satisfiability { } } -fn add_normalized_clause(clause: &CNFClause, next_var: &mut i32, normalized: &mut Vec) { +fn add_normalized_clause( + clause: &CNFClause, + variables: &mut SatVariableAllocator, + normalized: &mut Vec, +) -> 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 +54,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 = (*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 +78,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) { @@ -106,20 +109,28 @@ impl ReduceTo 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..66a7ba122 100644 --- a/src/rules/satisfiability_naesatisfiability.rs +++ b/src/rules/satisfiability_naesatisfiability.rs @@ -9,6 +9,7 @@ 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. @@ -53,8 +54,11 @@ impl ReduceTo 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 = self .clauses() @@ -72,7 +76,7 @@ impl ReduceTo 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

(problem: &P, lower: i32, upper: i32) -> Option +fn solve_via_decision_min

(problem: &P, lower: i64, upper: i64) -> Option where - P: DecisionProblemMeta + Problem> + Clone, + P: DecisionProblemMeta + Problem> + Clone, { if lower > upper { return None; @@ -42,9 +42,9 @@ where Some(lo) } -fn solve_via_decision_max

(problem: &P, lower: i32, upper: i32) -> Option +fn solve_via_decision_max

(problem: &P, lower: i64, upper: i64) -> Option where - P: DecisionProblemMeta + Problem> + Clone, + P: DecisionProblemMeta + Problem> + Clone, { if lower > upper { return None; @@ -70,15 +70,15 @@ where #[doc(hidden)] pub trait DecisionSearchValue: - OptimizationValue + Clone + fmt::Debug + Serialize + DeserializeOwned + OptimizationValue + Clone + fmt::Debug + Serialize + DeserializeOwned { - fn solve_problem

(problem: &P, lower: i32, upper: i32) -> Option + fn solve_problem

(problem: &P, lower: i64, upper: i64) -> Option where P: DecisionProblemMeta + Problem + Clone; } -impl DecisionSearchValue for Min { - fn solve_problem

(problem: &P, lower: i32, upper: i32) -> Option +impl DecisionSearchValue for Min { + fn solve_problem

(problem: &P, lower: i64, upper: i64) -> Option where P: DecisionProblemMeta + Problem + Clone, { @@ -86,8 +86,8 @@ impl DecisionSearchValue for Min { } } -impl DecisionSearchValue for Max { - fn solve_problem

(problem: &P, lower: i32, upper: i32) -> Option +impl DecisionSearchValue for Max { + fn solve_problem

(problem: &P, lower: i64, upper: i64) -> Option where P: DecisionProblemMeta + Problem + Clone, { @@ -96,7 +96,7 @@ impl DecisionSearchValue for Max { } /// Recover an optimization value by querying the problem's decision wrapper. -pub fn solve_via_decision

(problem: &P, lower: i32, upper: i32) -> Option +pub fn solve_via_decision

(problem: &P, lower: i64, upper: i64) -> Option 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 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..54573115c 100644 --- a/src/unit_tests/models/formula/sat.rs +++ b/src/unit_tests/models/formula/sat.rs @@ -106,7 +106,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> { 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> { 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> { 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) { 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> { Decision::new( MinimumVertexCover::new( 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); +} 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::>::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::::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::(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 _ = + >>::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) -> String { + if let Some(message) = panic.downcast_ref::() { + return message.clone(); + } + panic + .downcast_ref::<&str>() + .expect("panic payload must be a string") + .to_string() +}