exact-solve

exact-solve computes the exact rational solution of an integer linear system A x = b on INT8 tensor cores, and is loadable through kernels. A ([n, n]) and b ([n, c]) are integer; the solution is returned as fractions.Fraction. It uses high-order Dixon p-adic lifting on the residue (CRT) engine shared with exact-gemm, fp64-emu, and fp128-emu.

Past a condition number of about 10^16 a double-precision solve returns noise in every component. Exact rational solving has no conditioning to lose: it returns the true numerators and denominators. It has been a CPU library operation, and this kernel puts the lift on tensor cores.

The order-30 Pascal system, condition ~10^32. fp64 returns every component wrong, off by up to 10^12 and in sign; exact-solve returns the true 18-digit integer solution (Pascal is unimodular, so the rationals are integers), verified A @ x == b in integer arithmetic, in 4 ms.

Usage

import torch
from kernels import get_kernel

es = get_kernel("phanerozoic/exact-solve", version=1, trust_remote_code=True)

A = torch.randint(-10**6, 10**6, (256, 256), dtype=torch.int64, device="cuda")
b = torch.randint(-10**6, 10**6, (256, 1), dtype=torch.int64, device="cuda")
X = es.solve(A, b)                 # [256][1] list of fractions.Fraction (exact)

b may have multiple columns. solve returns None when A is singular over the rationals, and raises when the input falls outside the range below. gmpy2 accelerates the CPU reconstruction path.

API

Method

Dixon (1982) recovers the exact solution from a p-adic expansion: with B = A^{-1} mod P, r_0 = b, and x_i = B r_i mod P, r_{i+1} = (r_i - A x_i) / P, the digits x_i reconstruct x once the precision P^m exceeds twice the Hadamard bound on numerator and denominator.

The modulus is a squarefree product P = prod(q_j) over primes q_j < 256. Each step's A^{-1} mod q_j applied to the residual is then a native INT8 tensor-core GEMM, one per prime, and balanced-Garner reconstruction assembles the wide base-P digit directly. A product of primes in place of a single word prime divides the sequential step count by the prime count (~460 word-prime steps at n = 256 become ~44), which is what puts the lift on the tensor cores rather than in a long scalar recurrence.

The batched modular inverse takes A^{-1} mod q_j for every prime by Gauss-Jordan over the augmented matrix, one grid per elimination step spanning all primes, with Barrett reduction in place of hardware modulo and a table of pivot inverses in place of a search. The lift issues each step's per-prime products as one batched INT8 GEMM, CRT-reconstructs the wide digit, and carries the residual in a single limb as (r_i - A x_i) P^{-1} mod 2^64, P odd.

Reconstruction takes a common denominator d from components sampled per right-hand side and recovers every entry in one device pass as num = balanced(X d mod P^m), with X the Horner sum of that entry's p-adic digits. A denominator carrying a factor outside d drives its numerator past the bound N, so the bound check certifies each entry; the rest fall to their own extended-Euclid, and d widens from the failures for one repeat pass when the sample missed a large share of the grid. Systems whose scratch exceeds the device budget reconstruct on the CPU, one extended-Euclid per entry.

Measured

Median wall-clock of the full solve against FLINT fmpq_mat.solve on the same host, 24-bit integer entries.

RTX PRO 6000 Blackwell / NVIDIA H200:

The single-RHS crossover is near n = 256. The same ordering holds on L4.

Correctness

tests/test_exact_solve.py compares against an exact Fraction Gaussian-elimination oracle, the integer identity A @ N == d * b (numerators N, common denominator d), a planted integer solution, a scaled-Hilbert system with dense denominators, and a repeat call for determinism.

Requirements and limits

• NVIDIA GPU with compute capability 8.0+ and torch with INT8 tensor-core GEMM.
• Integer A [n, n], b [n, c], with n * max|A_ij| < 2^63 and n <= 2^17. Dtype, shape and both bounds are checked.
• Dixon needs one prime that does not divide det(A). A determinant divisible by every prime below 256 leaves the lift no modulus, and raises.
• Working memory scales with the prime count and n; the batched inverse holds an augmented [E, n, 2n] int32 buffer.

References

Dixon, "Exact solution of linear equations using p-adic expansions" (Numerische Mathematik 40, 1982); Ozaki, Ogita, Oishi, Rump 2012 (Numerical Algorithms 59); Ozaki, Uchino, Imamura 2025 (Ozaki Scheme II, arXiv:2504.08009); Hart et al., FLINT (Fast Library for Number Theory).

License

Apache-2.0.