Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
- René Thiemann
- Jose Divasón
- Ralph Bottesch
ISSN: 2150-914x
Año de publicación: 2021
Páginas: 1-418
Tipo: Artículo
Proyectos relacionados
Resumen
We verify two algorithms for which modular arithmetic plays an essential role: Storjohann's variant of the LLL lattice basis reduction algorithm and Kopparty's algorithm for computing the Hermite normal form of a matrix. To do this, we also formalize some facts about the modulo operation with symmetric range. Our implementations are based on the original papers, but are otherwise efficient. For basis reduction we formalize two versions: one that includes all of the optimizations/heuristics from Storjohann's paper, and one excluding a heuristic that we observed to often decrease efficiency. We also provide a fast, self-contained certifier for basis reduction, based on the efficient Hermite normal form algorithm.