FACT- and SAT-solvers on different types of semiprimes

Abstract: This thesis is aimed to cover how boolean satisfiability solvers can be used on integer factorization problems and to compare them with already established integer factorization solvers. The integer factorization problem is believed to be hard and is used in modern day cryptoalgorithms such as RSA. This thesis is also aimed to explore how well different solvers can solve different types of semiprimes and if there is any notable difference between them. This report covers three different boolean satisfiability solvers as well as three of the integer factorization solvers. The results from the thesis show that boolean satisfiability solvers cannot be used as a replacement of already established integer factorization solvers. The thesis also shows that the type of semiprime does affect how fast the solvers are able to factorize the semiprime. The boolean satisfiability solvers had favorable results toward asymmetrical semiprimes and disfavorable results toward prime powers.