Satisfiability Solving and Lattice Reduction for Integer Factorization - Colloquium Series by: Dr. Curtis Bright

Abstract: In recent years, satisfiability (SAT) solvers have been increasingly used to solve a wide variety of problems in computational discrete mathematics. 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. We show that incorporating computer algebraic routines based on lattice basis reduction significantly speeds up SAT solvers on integer factorization problems. This work appeared in the Master's thesis of Yameen Ajani.