Skip to content

Separate CVP integer and floating-point variants under the numeric contract #1146

Description

@isPANN

Objective

Implement two CVP numeric variants under the repository's numeric contract: an integer variant for exact reductions and a floating-point variant for numerical modeling and solving. Keep one problem family and use the existing variant mechanism; define arithmetic separately for each concrete variant.

Public contract

For column basis B and integer coefficient vector x, evaluate squared Euclidean distance D(x) = sum_i ((Bx)_i - t_i)^2.

Contract ClosestVectorProblem ClosestVectorProblem
Basis entries and target coordinates i64 finite f64
Solution coefficients Vec Vec
Objective Min, squared distance Min, squared distance
Decision bound i64 squared-distance bound finite f64 squared-distance bound
Evaluation arithmetic Exact integer arithmetic; explicit overflow Ordinary f64 arithmetic and rounding; explicit non-finite-result errors
Reduction role Default variant for exact mathematical reductions Only rules explicitly justified for floating-point semantics

The float variant still describes a lattice: coefficients are integers, not real optimization variables. The numeric parameter covers both basis and target, rather than only the target. Use the existing coefficient variant naming convention (coefficient) consistently in registration, schemas, and callers; keep i64 as the default.

Neither public objective exposes BigInt or BigRational. Implementation-local exact arithmetic remains permitted, including integer solver orthogonalization, rank checks, and search state. Do not widen public results or silently fall back to another numeric variant.

Two worked examples

1. Integer variant: solve SubsetSum through a CVP reduction

Given item sizes {3, 5, 7} and target sum 8, construct the existing binary-carry reduction to Decision<ClosestVectorProblem<i64>>, solve the target, and recover the selected subset.

source sizes           = [3, 5, 7]
source target          = 8
CVP basis columns      = 6  (3 selection variables + 3 binary carries)
CVP ambient dimension  = 10 (6 selection rows + 4 sum-bit rows)
CVP target             = [0,0,0, 1,1,1, 1,0,0,0]
squared-distance bound = 3
CVP solution           = [1,1,0, 1,1,1]
recovered selection    = [true, true, false]
recovered subset       = {3, 5}

The first three coefficients select items; the remaining coefficients are carries ordered from the highest bit to the lowest. Each selection variable contributes x_i^2 + (x_i - 1)^2, at least 1 and equal to 1 exactly at 0 or 1. The sum-bit residuals vanish for this witness, so its squared distance is 3, attaining the lower bound. Recovering the first three coefficients gives 3 + 5 = 8.

This is the main integer workflow: construct a mathematical reduction, solve its target, and recover and verify the source solution. The example should use the actual registered reduction rather than a separate hand-written encoding.

2. Floating-point variant: quantize a point onto an oblique grid

Suppose a two-dimensional grid is generated by horizontal steps of (1.0, 0.0) and slanted steps of (0.5, 0.8). Snap the measured point (1.6, 0.9) to the nearest grid point.

basis columns = [[1.0, 0.0], [0.5, 0.8]]
target        = [1.6, 0.9]
solution      = [1, 1]
lattice point = [1.5, 0.8]
squared distance ≈ 0.02

The closest point is (1.5, 0.8): the vertical coordinate selects row 1, then the nearest horizontal position selects coefficient 1. This illustrates why a float basis and target are useful for geometric input while solution coefficients remain integers. Show construction, numerical solving, and evaluation through the typed API and CLI. Use ordinary f64 results; do not require exact equality to the decimal 0.02. Preserve the numerical solver's Feasible status rather than deriving a general optimality guarantee from this hand-checkable example.

Implementation plan

1. Separate model arithmetic and construction

  • Store basis: Vec<Vec<T>> and target: Vec<T> in the existing CVP family. Implement the concrete i64 and f64 Problem contracts separately; share structural code only where behavior is identical.
  • Remove the public ClosestVectorTarget::to_rational() transport contract and its unused exports. Do not replace it with a generic numeric adapter or dispatch framework.
  • Preserve dimension, witness-length, and full-column-rank checks. Reject nonfinite float inputs at construction/deserialization. Rank validation may retain implementation-local exact arithmetic over the stored coordinates; numerical difficulty in a solver is a separate SolveError, not permission to change model feasibility.
  • Integer evaluation uses checked i64 multiplication, addition, subtraction, squaring, and accumulation. Keep all observable results i64; an overflowing arithmetic step returns EvaluationError::IntegerOverflow. Do not promise that cancellation after an overflowing intermediate makes the computation acceptable.
  • Float evaluation uses finite f64 multiplication, addition, subtraction, squaring, and accumulation in a documented deterministic order. Reject nonfinite intermediate/results. Do not rationalize the public float objective or introduce tolerances into model feasibility.
  • Keep squared distance as the sole objective; document that bounds are squared-distance bounds, not ordinary distances.

2. Keep integer solving exact; separate numerical float solving

  • Retain exact Gram–Schmidt and sphere-enumeration arithmetic in the integer solver. Preserve the existing large-translation and nearly-parallel-basis regression cases introduced in commit e1a45a7.
  • Use BigInt for internal search coefficients, steps, and incumbents. Check conversion to Vec when returning the selected optimum. A genuine returned-coefficient overflow is an explicit SolveError; overflow in a temporary search step must not reject a representable optimum.
  • Public outcome construction must still evaluate through the integer model and propagate its checked-arithmetic errors.
  • Give the float variant a separate numerical sphere-enumeration path using its float basis and target. Report numerical breakdown, nonfinite arithmetic, or unrepresentable coefficient conversion explicitly. Do not fall back to the integer variant or silently substitute exact public semantics.
  • Return float numerical candidates as the existing SolveOutcome::Feasible, not an unproved Optimal. The current customized registration callback returns Option and the resolver upgrades every witness to Optimal. Replace that callback result with the existing outcome representation, update its existing registrations, and preserve statuses directly; do not add another solver registry or a second parallel interface.
  • Exact customized solvers retain their current Optimal/Infeasible behavior. Rules requiring an optimum must reject an insufficient-quality float result using existing recovery errors.

3. Decision and reduction consumers

  • Register Decision<CVP> with i64 bounds and Decision<CVP> with finite f64 bounds using existing Decision infrastructure.
  • Preserve the exact integer decision solver. Do not register a complete float decision solver based only on the numerical optimizer: a candidate meeting the bound proves YES, but a candidate missing it does not prove NO. Float decision construction/evaluation remains available without inventing an inconclusive-as-infeasible fallback.
  • Keep SubsetSum -> Decision<CVP>. Convert the item count to i64 with a checked conversion and use n as the squared-distance bound.
  • Keep CVP -> QUBO; audit construction arithmetic, recovery, and objective comparisons under the i64 objective contract. Do not mechanically register an analogous float rule.
  • Remove the existing CVP -> CVP exact variant edge and its paper/catalog entry. Lossless input-coordinate conversion alone does not establish preservation of floating-point objective ordering. Do not add a reverse rounded conversion or an unrelated numerical-conversion subsystem.

4. Public integration and documentation

  • Update construction specs, persisted schemas, variant metadata, CLI/MCP creation, outcome serialization/formatting, example-db entries, and typed callers together.
  • Replace rational decision bounds and rational-value fixtures with the concrete variant's numeric type.
  • Update docs/src/design.md to replace the CVP public-BigRational exception with these two contracts. Update the paper definition, decision entries, reduction statements, and examples consistently.
  • Replace changed behavior directly. Do not retain old target-only variant aliases, rational-objective compatibility wrappers, or deprecated parallel implementations.

Acceptance and verification

Primary workflows

  • Run the SubsetSum example through the actual registered integer reduction, solve the CVP decision target, recover {3, 5}, and verify the source sum is 8. Cover an ordinary small NO instance as well.
  • Construct and solve the oblique-grid float example through typed and CLI paths; obtain coefficients [1, 1], reconstruct (1.5, 0.8), and evaluate squared distance approximately 0.02.
  • Verify both variants expose the correct basis, target, objective, and bound types in construction schemas and serialization; round-trip ordinary instances.
  • Check integer SubsetSum/CVP/QUBO recovery and ordinary decision thresholds, including tied witnesses where relevant.
  • Verify the resolver preserves the float solver's Feasible status and optimum-dependent recovery rejects insufficient solution quality.
  • Verify catalog reachability no longer advertises the removed cross-variant edge.

Focused implementation regressions

  • Preserve existing regressions that reproduce actual integer-search defects, including the historical pruning failures; add a focused check for the identified internal coefficient-step overflow.
  • Verify required typed errors for integer arithmetic/output overflow, nonfinite float input/results, and numerical solver failure. Keep these checks subordinate to the main modeling/reduction/solving workflows; do not expand this task into an extreme-value test campaign.

Run focused model/solver/reduction/decision and CLI/MCP checks, then make check and the required changed-line coverage gate; validate affected paper/examples. If the implementation PR exceeds 20 changed files or 1,000 added lines, stop for scope confirmation under repository policy.

Historical rationale and scope

  • Commit e1a45a77 introduced exact arithmetic inside the solver with concrete pruning regressions. Preserve that correctness work in integer solving.
  • Commit 0bc59e46 extended rational arithmetic to public CVP objectives, conversion, and dependent comparisons. This plan defines separate public numeric contracts while retaining necessary internal arithmetic.
  • Use existing dependencies and outcome/error types. No new backend, numeric framework, compatibility layer, or automatic cross-variant routing.

Related: #1141, #1145.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions