<p>Extending what @Amir wrote, I came across the following nice web page which hosts a <a href="http://cgi.cs.indiana.edu/~sabry/cnf.html">CNF generator for factoring circuits</a> that one could e.g. run on some of the (now inactive) <a href="http://en.wikipedia.org/wiki/RSA_Factoring_Challenge">RSA Factoring Challenge</a> <a href="http://en.wikipedia.org/wiki/RSA_numbers">numbers</a>. The generated instances are in <a href="http://www.satlib.org/Benchmarks/SAT/satformat.ps">DIMACS</a> format that can directly be fed to any one of the current competitors in the annual <a href="http://www.satcompetition.org/2011/">SAT</a> <a href="http://baldur.iti.uka.de/sat-race-2010/">solver</a> <a href="http://www.satcompetition.org/">competition</a>. Regarding hard SAT instances in general, the benchmark problems given at the SAT competition site appear to be quite useful, also the classification into random/crafted/industrial is nice. </p>

CC BY-SA 3.0
2011-05-28T16:23:29.770Z
That link is very cool!
Huck Bennett
CC BY-SA 3.0
2014-12-09T03:10:06.237Z
If you actually try inputting one of those numbers you'll find their source code uses the int datatype and therefore can only hold 32-bit numbers, while the unfactored RSA numbers start at hundreds of bits.
Elliot Gorokhovsky
CC BY-SA 3.0
2011-05-27T07:11:22.140Z
2011-05-27T08:34:01.477Z
2011-05-27T08:34:01.477Z
Martin Schwarz
<p>Here's a paper on generating SAT instances from factoring:</p>

<p>Horie, S. &amp; Watanabe, O. [1997] "<a href="http://www.springerlink.com/content/n0280u3767nl14w4/">Hard instance generation for SAT</a>" <em>Algorithms and Computation</em> 1350:22-31 (<a href="http://arxiv.org/pdf/cs/9809117">pdf</a>)</p>

<p>It's worse than linear, but better than $n^2$.  A 512-bit RSA challenge type number generates an instance with 63,652 variables and 406,860 clauses.</p>

CC BY-SA 3.0
2011-06-01T18:59:27.333Z
2012-07-22T00:53:20.140Z
2012-07-22T00:53:20.140Z
Lou Scheffer
<p><a href="http://toughsat.appspot.com/">ToughSat</a> by Henry Yuen and Joseph Bebel is another tool similar to the one linked by @Martin, which generates CNF formulas that encode instances of factoring and other hard problems.</p>

CC BY-SA 3.0
2011-06-08T15:19:45.500Z
Scott blogged about this too: http://www.scottaaronson.com/blog/?p=676
Alessandro Cosentino
CC BY-SA 3.0
2011-06-06T19:12:28.473Z
2011-06-06T19:12:28.473Z
Alessandro Cosentino
<p>you can (batch) generate very efficient DIMACS files of any bit-size with Paul Purdom and Amr Sabry's CNF Generator <strong>locally now</strong> with this <a href="https://github.com/GridSAT/CNF_FACT-MULT" rel="nofollow noreferrer">GitHub repo</a> which is also available on IPFS ipfs://QmYuzG46RnjhVXQj7sxficdRX2tUbzcTkSjZAKENMF5jba</p>
<p>the percentage of new VARs decreases with increasing bit-sizes:
<a href="https://i.sstatic.net/3F2To.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/3F2To.png" alt="CNF Generator % new VARs vs. bits" /></a></p>

CC BY-SA 4.0
2024-04-21T22:59:23.947Z
2024-04-21T22:59:23.947Z
alephc
<p>See <a href="https://github.com/sjneph/satfactor" rel="nofollow noreferrer"><code>satfactor</code></a>:
<hr></p>

<h2>Convert Integer Factorization into a boolean SATISFIABILITY problem</h2>

<blockquote>
  <p>Shane Neph</p>
</blockquote>

<h1>Overview</h1>

<p>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.</p>

<h1>What this code does</h1>

<p>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.</p>

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

<p>This project has 2 main purposes:<br>
1) Convert the problem and factor an integer of interest!<br>
2) Quickly create either a solvable or an unsolvable SATISFIABILITY problem, whose difficulty is easily controlled by the creater.<br>
- To create an unsolvable SATISFIABILITY problem, simply encode a prime number.<br>
- To create more difficult but solvable problems, choose larger composite numbers with fewer factors.  </p>

<p>The number of interest may be any size! </p>

<p>There are some open-source SATISFIABILITY solvers.  See <a href="http://www.satlive.org/" rel="nofollow noreferrer">http://www.satlive.org/</a> for some of these.</p>

<h1>Build</h1>

<p>make -C src/</p>

<h1>How-To</h1>

<p>Input a number of interest in its binary form: </p>

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

<p>The output would be:<br>
00011<br>
00111 </p>

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

<p>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).</p>

<p>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 any number of lines).  For example, </p>

<p>1 -2 3 4 -5 ...</p>

CC BY-SA 4.0
2018-09-15T05:44:39.160Z
Can you summarize the techniques used by this software?  On this site we are more interested in algorithms and techniques, rather than an advertisement of a software tool.  For example, the questions for the complexity of the reduction.  I don't see how you've addressed the question; on Stack Exchange sites, you should only answer if you can answer the specific question that was asked.  Also, do you have any relationship with the tool or its authors?
D.W.
CC BY-SA 4.0
2018-09-15T04:44:06.770Z
2018-09-15T04:44:06.770Z
Geremia
<p>One approach to encode Factoring (RSA) to SAT is to use multiplicator circuits (every circuit can be encoded as CNF).</p>
<p>Let's assume we are given an integer <span class="math-container">$C$</span> with <span class="math-container">$2n$</span> bits, <span class="math-container">$C=(c_1,c_2,\cdots,c_{2n})_2$</span>. We are interested in finding two <span class="math-container">$n$</span>-bit integers <span class="math-container">$A=(a_1,\cdots,a_n)$</span> and <span class="math-container">$B=(b_1,\cdots,b_n)$</span> whose product is <span class="math-container">$C=A*B$</span>.</p>
<p>The most naive encoding can be something like this; we know that:</p>
<p><span class="math-container">$$c_{2n}= a_n \land b_n$$</span>
<span class="math-container">$$c_{2n-1}= (a_n\land b_{n-1}) xor (a_{n-1}\land b_n)$$</span>
<span class="math-container">$$Carry:d_{2n-1}= (a_n\land b_{n-1}) \land (a_{n-1}\land b_n)$$</span>
<span class="math-container">$$c_{2n-2}= (a_n\land b_{n-2}) xor (a_{n-1}\land b_{n-1}) xor (a_{n-2}\land b_{n}) xor d_{2n-1}$$</span>
...</p>
<p>Then using Tseitin transformation, the above encoding can be translated into CNF.</p>
<p>This approach produces a relatively small CNF. But this encoding does not support &quot;Unit Propagation&quot; and so, the performance of SAT Solvers are really bad.</p>
<p>There are other circuit for multiplication which can be used for this purpose, but they produce a larger CNF.</p>

CC BY-SA 3.0
2011-05-27T06:29:56.990Z
In section 6.1 of "Finding Hard Instances of the Satisfiability problem: A survey", by Cook and Mitchell, they use this problem as a challenge.
Amir
CC BY-SA 3.0
2013-10-17T13:14:27.103Z
How do you know that A and B must be n bits length, couldn't it be n - 1 and and n bits. For sure it can be 2n bits and 1 bit.
Ilya Gazman
CC BY-SA 3.0
2013-10-17T19:40:28.857Z
@Babibu: If we are talking about general factorization, you are right. But for case of RSA, we know that each of the two primes has $n$ bits.
Amir
CC BY-SA 3.0
2013-11-11T08:06:42.060Z
I understand you answer but I don't know how to continue it. Can you please show $c_{2n−2}$.
Ilya Gazman
CC BY-SA 3.0
2013-11-28T23:41:26.660Z
What about [RSA-129](http://en.wikipedia.org/wiki/RSA_numbers#RSA-129)
Ilya Gazman
CC BY-SA 4.0
2011-05-27T06:24:13.503Z
2020-08-04T16:14:29.183Z
2020-08-04T16:14:29.183Z
Amir
<p>Scott Aaronson's <a href="http://www.scottaaronson.com/blog/?p=663">blog post</a> today gave a list of interesting open problems/tasks in complexity. One in particular caught my attention:</p>

<blockquote>
  <p>Build a public library of 3SAT instances, with as few variables and clauses as possible, that would have noteworthy consequences if solved.  (For example, instances encoding the RSA factoring challenges.)  Investigate the performance of the best current SAT-solvers on this library.</p>
</blockquote>

<p>This triggered my question: What's the standard technique for reducing RSA/factoring problems to SAT, and how fast is it? Is there such a standard reduction?</p>

<p>Just to be clear, by "fast" I don't mean polynomial time. I'm wondering whether we have tighter upper bounds on the reduction's complexity. For example, is there a known cubic reduction?</p>

<cc.complexity-theory><cr.crypto-security><sat><reductions><factoring>
Fast Reduction from RSA to SAT
Huck Bennett
# Fast Reduction from RSA to SAT

(Asked by: username_0 on 2011-05-27)

Scott Aaronson's [blog post](http://www.scottaaronson.com/blog/?p=663) today gave a list of interesting open problems/tasks in complexity. One in particular caught my attention:

> Build a public library of 3SAT instances, with as few variables and clauses as possible, that would have noteworthy consequences if solved. (For example, instances encoding the RSA factoring challenges.) Investigate the performance of the best current SAT-solvers on this library.

This triggered my question: What's the standard technique for reducing RSA/factoring problems to SAT, and how fast is it? Is there such a standard reduction?

Just to be clear, by "fast" I don't mean polynomial time. I'm wondering whether we have tighter upper bounds on the reduction's complexity. For example, is there a known cubic reduction?

**Tags:** cc.complexity-theory, cr.crypto-security, sat, reductions, factoring

---

## 6 answers

### Answer by username_8 on 2011-05-27. Score: 32 | Accepted answer

One approach to encode Factoring (RSA) to SAT is to use multiplicator circuits (every circuit can be encoded as CNF).

Let's assume we are given an integer $C$ with $2n$ bits, $C=(c\_1,c\_2,\cdots,c\_{2n})\_2$. We are interested in finding two $n$-bit integers $A=(a\_1,\cdots,a\_n)$ and $B=(b\_1,\cdots,b\_n)$ whose product is $C=A\*B$.

The most naive encoding can be something like this; we know that:

$$c\_{2n}= a\_n \land b\_n$$
$$c\_{2n-1}= (a\_n\land b\_{n-1}) xor (a\_{n-1}\land b\_n)$$
$$Carry:d\_{2n-1}= (a\_n\land b\_{n-1}) \land (a\_{n-1}\land b\_n)$$
$$c\_{2n-2}= (a\_n\land b\_{n-2}) xor (a\_{n-1}\land b\_{n-1}) xor (a\_{n-2}\land b\_{n}) xor d\_{2n-1}$$
...

Then using Tseitin transformation, the above encoding can be translated into CNF.

This approach produces a relatively small CNF. But this encoding does not support "Unit Propagation" and so, the performance of SAT Solvers are really bad.

There are other circuit for multiplication which can be used for this purpose, but they produce a larger CNF.

> **Comments:**
> **username_8**: In section 6.1 of "Finding Hard Instances of the Satisfiability problem: A survey", by Cook and Mitchell, they use this problem as a challenge.  
> **username_9**: How do you know that A and B must be n bits length, couldn't it be n - 1 and and n bits. For sure it can be 2n bits and 1 bit.  
> **username_8**: @Babibu: If we are talking about general factorization, you are right. But for case of RSA, we know that each of the two primes has $n$ bits.  
> **username_9**: I understand you answer but I don't know how to continue it. Can you please show $c_{2n−2}$.  
> **username_9**: What about [RSA-129](http://en.wikipedia.org/wiki/RSA_numbers#RSA-129)  

---

### Answer by username_1 on 2011-05-27. Score: 23

Extending what @Amir wrote, I came across the following nice web page which hosts a [CNF generator for factoring circuits](http://cgi.cs.indiana.edu/~sabry/cnf.html) that one could e.g. run on some of the (now inactive) [RSA Factoring Challenge](http://en.wikipedia.org/wiki/RSA_Factoring_Challenge) [numbers](http://en.wikipedia.org/wiki/RSA_numbers). The generated instances are in [DIMACS](http://www.satlib.org/Benchmarks/SAT/satformat.ps) format that can directly be fed to any one of the current competitors in the annual [SAT](http://www.satcompetition.org/2011/) [solver](http://baldur.iti.uka.de/sat-race-2010/) [competition](http://www.satcompetition.org/). Regarding hard SAT instances in general, the benchmark problems given at the SAT competition site appear to be quite useful, also the classification into random/crafted/industrial is nice.

> **Comments:**
> **username_0**: That link is very cool!  
> **username_2**: If you actually try inputting one of those numbers you'll find their source code uses the int datatype and therefore can only hold 32-bit numbers, while the unfactored RSA numbers start at hundreds of bits.  

---

### Answer by username_3 on 2011-06-01. Score: 17

Here's a paper on generating SAT instances from factoring:

Horie, S. & Watanabe, O. [1997] "[Hard instance generation for SAT](http://www.springerlink.com/content/n0280u3767nl14w4/)" *Algorithms and Computation* 1350:22-31 ([pdf](http://arxiv.org/pdf/cs/9809117))

It's worse than linear, but better than $n^2$. A 512-bit RSA challenge type number generates an instance with 63,652 variables and 406,860 clauses.


---

### Answer by username_4 on 2011-06-06. Score: 11

[ToughSat](http://toughsat.appspot.com/) by Henry Yuen and Joseph Bebel is another tool similar to the one linked by @Martin, which generates CNF formulas that encode instances of factoring and other hard problems.

> **Comments:**
> **username_4**: Scott blogged about this too: http://www.scottaaronson.com/blog/?p=676  

---

### Answer by username_5 on 2024-04-21. Score: 2

you can (batch) generate very efficient DIMACS files of any bit-size with Paul Purdom and Amr Sabry's CNF Generator **locally now** with this [GitHub repo](https://github.com/GridSAT/CNF_FACT-MULT) which is also available on IPFS ipfs://QmYuzG46RnjhVXQj7sxficdRX2tUbzcTkSjZAKENMF5jba

the percentage of new VARs decreases with increasing bit-sizes:
[![CNF Generator % new VARs vs. bits](https://i.sstatic.net/3F2To.png)](https://i.sstatic.net/3F2To.png)


---

### Answer by username_6 on 2018-09-15. Score: 0

See [`satfactor`](https://github.com/sjneph/satfactor):

---

## Convert Integer Factorization into a boolean SATISFIABILITY problem

> Shane Neph

# Overview

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.

# What this code does

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.

# Build

make -C src/

# How-To

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 any number of lines). For example,

1 -2 3 4 -5 ...

> **Comments:**
> **username_7**: Can you summarize the techniques used by this software?  On this site we are more interested in algorithms and techniques, rather than an advertisement of a software tool.  For example, the questions for the complexity of the reduction.  I don't see how you've addressed the question; on Stack Exchange sites, you should only answer if you can answer the specific question that was asked.  Also, do you have any relationship with the tool or its authors?  

---

