Cargando…
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL
The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattic...
Autores principales: | Thiemann, René, Bottesch, Ralph, Divasón, Jose, Haslbeck, Max W., Joosten, Sebastiaan J. C., Yamada, Akihisa |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
Springer Netherlands
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7413592/ https://www.ncbi.nlm.nih.gov/pubmed/32831440 http://dx.doi.org/10.1007/s10817-020-09552-1 |
Ejemplares similares
-
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL
por: Bottesch, Ralph, et al.
Publicado: (2020) -
A Verified Implementation of Algebraic Numbers in Isabelle/HOL
por: Joosten, Sebastiaan J. C., et al.
Publicado: (2018) -
Lattice basis reduction: an introduction to the LLL algorithm and its applications
por: Bremner, Murray R
Publicado: (2012) -
The LLL algorithm: survey and applications
por: Nguyen, Phong Q, et al.
Publicado: (2010) -
N-Dimensional LLL Reduction Algorithm with Pivoted Reflection
por: Deng, Zhongliang, et al.
Publicado: (2018)