Modular_arithmetic_LLL_and_HNF_algorithms (Q5974233)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Modular_arithmetic_LLL_and_HNF_algorithms
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Modular_arithmetic_LLL_and_HNF_algorithms |
AFP entry Modular_arithmetic_LLL_and_HNF_algorithms |
Statements
Ralph Bottesch
0 references
Jose Divasón
0 references
René Thiemann
0 references
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.
0 references
12 March 2021
0 references
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation (English)
0 references
