Factorization patterns in 3-SAT : Analysis of clause ordering for reductions of the integer factorization problem

Abstract: Dividing a large integer into factors is a well-known difficult problem that is heavily used in modern cryptography. One approach to achieve faster factorizations is to reduce the Integer factorization problem to another difficult problem, for example the Boolean satisfiability problem. Many studies have been done on the optimization of algorithms that can solve the Boolean satisfiability problem effectively and multiple programs have been created for the purpose of achieving efficiency. This study focuses on one of these programs, MiniSAT, with the objective of finding patterns in the input that result in faster runtimes for solving reduced instances of the Integer factorization problem. The method used for finding these patterns was to create different reductions from the Integer factorization problem to the Boolean satisfiability problem and then solving the reduced instances using MiniSAT. The order of the clauses in the boolean formulas were changed in order to analyze which order yields the best results. In total, seven orderings were tested for factorizing four products using three different reductions. Our conclusions are that none of the patterns lead to better results for every test case. Not changing the order of the clauses will achieve consistent results, however there are cases when shuffles with variance could be preferable.