A verified factorization algorithm for integer polynomials with polynomial complexity (Q7361900)
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 LLL_Factorization
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A verified factorization algorithm for integer polynomials with polynomial complexity |
AFP entry LLL_Factorization |
Statements
6 February 2018
0 references
Jose Divasón
0 references
Sebastiaan J. C. Joosten
0 references
René Thiemann
0 references
Akihisa Yamada
0 references
A verified factorization algorithm for integer polynomials with polynomial complexity (English)
0 references
Short vectors in lattices and factors of integer polynomials are related. Each factor of an integer polynomial belongs to a certain lattice. When factoring polynomials, the condition that we are looking for an irreducible polynomial means that we must look for a small element in a lattice, which can be done by a basis reduction algorithm. In this development we formalize this connection and thereby one main application of the LLL basis reduction algorithm: an algorithm to factor square-free integer polynomials which runs in polynomial time. The work is based on our previous Berlekamp–Zassenhaus development, where the exponential reconstruction phase has been replaced by the polynomial-time basis reduction algorithm. Thanks to this formalization we found a serious flaw in a textbook.
0 references
