MC 6460
Curtis Bright | University of Windsor
Title
SAT Solving with Lattice Reduction for Integer Factorization
Abstract
In recent years, satisfiability (SAT) solvers have been increasingly used to solve a wide variety of problems in computational discrete mathematics. For example, they were used as a part of the acclaimed discovery by Smith, Myers, Kaplan, and Goodman-Strauss of the "hat", the first aperiodic monotile [1].
In this talk, we overview the usage of SAT solving for problems in computational mathematics. In particular, we discuss how to apply SAT solvers to the problem of factoring an integer into its prime factors. In general, SAT solvers are not competitive with the best algebraic approaches for integer factorization, but when extra information is available—such as when some bits of the prime factors have been leaked—SAT solvers can outperform traditional approaches.
Moreover, the efficiency of SAT solvers on many problems in computational mathematics can be dramatically improved by incorporating computer algebraic routines exploiting mathematical structure unknown to the SAT solver [2]. We show that incorporating computer algebraic routines based on lattice basis reduction significantly speeds up SAT solvers on integer factorization problems. This work appeared at ISSAC 2024 and in the Master's thesis of Yameen Ajani [3].
[1] An Aperiodic Monotile. Combinatorial Theory 2024.
[2] When Satisfiability Solving Meets Symbolic Computation. Communications of the ACM 2022.
[3] SAT and Lattice Reduction for Integer Factorization. ISSAC 2024.