A restricted version of the COMPOSITE NUMBER problem was suggested as a challenge to satisfability solvers in 1997 by Cook and Mitchell [1]. The problem is this: Given a (2n)-bit number, determine the two n-bit prime factors. Part of the problem is the challenge of the encoding. There are a few encoders around, and instances have been presented in SAT competition before. The one used here is probably not the best one. See Horie, Watanabe [2] and Watanabe et al [3] for more examples and improvements.
The encoding program, written in "c", encodes a school method multiplication circuit. We didn't use a minimised circuit design (for example, as described by Wegener [4] ), because an encoding of "time" is required, and this causes additional complexity with overheads. The result (the product) is fixed, so a SAT solver must "reverse-engineer" the result through the multiplication circuit to find the prime factors. The primes used for the competition problems are with "probable" (1 - 2^-100 likely) primes using the java BigInteger class which provides an unspecified generating method (probably Rabin-Miller). The SAT instances produced by the encoder use (2n^2 + 2n - 1) variables and (20n^2 - 15n -1) clauses, though (3n+2) clauses are units.
All numbers used to encode the problems created for the 2004 SAT competition (excluding the separate two "Huge" examples) would be factored very quickly by state of the art factorisation methods. As a comparison some typical factorisation execution times, using a variant of the Multiple Polynomial Quadratic Sieve (MPQS) method on a 300 Mhz Ultrasparc 10, are shown below(*). The method uses two large primes (i.e. PPMPQS), which is faster than PMPQS or the basic MPQS, especially for larger numbers, though it uses more space. If the problem were factoring two n-bit primes then halving the numbers of digits shown in the table gives a rough comparison to the composite problem specification described above. It is highly unlikely that SAT solvers could reach this kind of performance on similar hardware architecture, not least because they do not utilise the hardware in the same way that factorisation algorithms can.
| Approximate Factorisation Times for n-bit Products using MPQS(*) |
| Decimal Digits | Binary Digits (approx) | Time (seconds) |
| 60 | 199 | 300 |
| 65 | 216 | 1,000 |
| 70 | 233 | 3,400 |
| 75 | 249 | 11,000 |
| 80 | 266 | 20,000 |
| 85 | 282 | 64,000 |
| 90 | 299 | 200,000 |
| 95 | 316 | 900,000 |
| 100 | 332 | 2,500,000 |
A recent overview and discussion of modern techniques of factoring algorithms can be found in Brent [5]. Recently, using the General Number Field Sieve (GNFS) method, a 576-bit number has been factored (see [6]). This number was part of the RSA Challenge. A 164-digit decimal number took the equivalent of 7 years on a 2.5Ghz Pentium to factor, also using the GNFS method (see [7]).
The results from the competition for the composite benchmark sets can be found here . The full set of competition results can be accessed and navigated through by starting from here.
The instances submitted to 2004 SAT competition and the code used to generate them is available:
(*)Thanks and gratitude to Richard Brent for his helpful comments, information, and supplying the factorisation execution times.
|
|
Last modified: Sat Feb 21 02:18:10 EST 2004