Shane Neph

Determining factors of a large integer number has been of interest to Man since at least Euclid's time. There is no known general algorithm for this problem that scales in less than exponential time with respect to the number of bits needed to represent the integer.

Converts an integer factorization problem into a boolean SATISFIABILITY problem. If the problem is solved by a SAT solver, it then extracts the integer factors.

Boolen satisfiability solvers improve every year. Every 2 years, an international competition between solvers takes place (see http://www.satcompetition.org/ and http://www.satlive.org/). How well can these state-of-the-art solvers do against one of the oldest open math problems in existence?

This project has 2 main purposes:

1. Convert the problem and factor an integer of interest!
2. Quickly create either a solvable or an unsolvable SATISFIABILITY problem, whose difficulty is easily controlled by the creater.

• To create an unsolvable SATISFIABILITY problem, simply encode a prime number.
• To create more difficult but solvable problems, choose larger composite numbers with fewer factors.

The number of interest may be any size!

There are some open-source SATISFIABILITY solvers. See http://www.satlive.org/ for some of these.

make -C src/

Input a number of interest in its binary form:

bin/iencode 10101 > composite.21
// solve with your favorite solver and put results in solution.txt
bin/extract-sat composite.21 solution.txt

The output would be:
00011
00111

which are binary representations for decimal integers 3 and 7, the factors of 21.

If an input integer has more than 2 factors, and the SAT problem is solved, the output will be two of the factors only. These may not be prime numbers (you could test for that easily in Maxima, Maple, or Mathematica).

Not all SAT solvers output results in the same format. You may need to doctor those results slightly. extract-sat requires a solution file containing a list of integers (on one line). For example,

1 -2 3 4 -5 ...