A comparison of reductions from FACT to CNF-SAT

Abstract: The integer factorisation problem (FACT) is a well-known number-theoreticproblem, with many applications in areas such as cryptography. An instanceof a FACT problem (a number n such that n = p × q) can be reduced to aninstance of the conjunctive normal form boolean satisfiability problem (CNFSAT),a well-known NP-complete problem. Some applications of this is toutilize advances in SAT solving for solving FACT, and for creating difficult CNF-SAT instances.This report compares four different reductions from FACT to CNF-SAT,based on the full adder, array multiplier and Wallace tree multiplier circuits.The comparisons were done by reducing a set of FACT instances to CNF-SAT instances with the different reductions. The resulting CNF-SAT instanceswere then compared with respect to the number of clauses and variables, aswell as the time taken to solve the instances with the SAT solver MiniSat.