[Rule] ClosestVectorProblem to QUBO

[GiggleLiu]

Source: ClosestVectorProblem<i32> (integer basis variant, #90)
Target: QUBO
Motivation: Enables solving CVP on quantum annealers and Ising machines via QUBO formulation.
Reference: Andersen & Yakubovich, "A QUBO model for the Closest Vector Problem", arXiv:2304.03616

Reduction Algorithm

Notation:

• Source instance: integer basis A ∈ Z^{m×n} with columns a₁, ..., aₙ, target vector t ∈ R^m, b = max|A_{ij}|
• Target instance: QUBO matrix Q ∈ R^{N×N}, where N = total binary variables
• G = AᵀA (Gram matrix), h = Aᵀt

Variable mapping:

1. For each integer coefficient x_i, derive bound K_i from the integer basis A (polynomial in n and b, per the paper).
2. Binary-encode each x_i ∈ {-K_i, ..., K_i} as x_i = -K_i + Σⱼ 2ʲ b_{i,j} using L_i = ⌈log₂(2K_i+1)⌉ binary variables.
3. Total binary variables: N = Σᵢ L_i.

Objective transformation:
The CVP objective ‖Ax - t‖₂² expands as:

‖Ax - t‖₂² = xᵀGx - 2hᵀx + tᵀt

Substitute x_i = -K_i + Σⱼ 2ʲ b_{i,j} into this quadratic form. After expanding, we obtain a quadratic function in the N binary variables b_{i,j}, which is directly a QUBO instance. The constant term tᵀt can be dropped (does not affect the optimal binary assignment).

Solution extraction:
Given optimal binary vector b*, reconstruct x_i = -K_i + Σⱼ 2ʲ b*_{i,j} for each i.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_vars	O(n²(log n + log b))
num_quadratic_terms	O(n⁴(log n + log b)²)

Validation Method

• Compare source/target optimal values on small instances using brute-force CVP solver and brute-force QUBO solver
• Cross-check with the example from [Model] ClosestVectorProblem #90
• Generate ground truth from ProblemReductions.jl: https://github.com/GiggleLiu/ProblemReductions.jl

Example

Use the 3D integer lattice from #90:

A = [[2, 1, 0], [0, 2, 1], [0, 0, 2]] (columns: a₁=(2,0,0), a₂=(1,2,0), a₃=(0,1,2))

b = max|A_{ij}| = 2

t = (3, 3, 3)

Gram matrix G = AᵀA = [[4, 2, 0], [2, 5, 2], [0, 2, 5]]
h = Aᵀt = (6, 9, 9)

Optimal CVP solution: x = (1, 1, 1), distance = 1. The QUBO instance should have the same minimum energy (up to constant tᵀt = 27) corresponding to x = (1, 1, 1) after binary decoding.