A comparison of reductions from FACT to CNF-SAT
John Eriksson, Jonas Höglund · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2014
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 (CNF-SAT), a well-known NP-complete problem. Some applications of this is toutilize advances in SAT solving for solving FACT, and for creating difficultCNF-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-SATinstances 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.