Introduction

In this work we focus on the problem of factoring semi-primes with SAT-solvers. A semi-prime N is a composite of two primes p and q which are roughly of equal size. These particular composites are conjectured to be hard to factor, in the sense that no (classical) algorithm or heuristic is known to factor semi-primes using only polynomially many resources. This problem has great relevance for the RSA cryptosystem1, a widely-deployed public-key cryptosystem. The RSA cryptosystem is founded upon the difficulty of factoring integers: the existence of an efficient factoring algorithm would completely break its security.

Some authors have proposed an alternative approach they refer to as quantum factoring. In this paper, we explain why these approaches, while potentially helpful for studying quantum SAT-solving, are not likely a viable approach to integer factorization and, very importantly, are not a meaningful benchmark for people interested in quantum cryptanalysis of cryptosystems based on the integer factorization problem.

We attempt to generously extrapolate the kinds of speed-ups one might expect for a range of quantum solvers, and find no evidence that this is a viable path toward factoring large numbers, even for scalable fault-tolerant quantum computers, as well as for various quantum annealing or other special purpose quantum hardware.

Some researchers only implement quantum factoring for the purposes of benchmarking the experimental apparatus. There are several more relevant algorithms to implement for the purposes of benchmarking, such as work on randomized benchmarking2 or implementations of quantum error correction. Framing the experiments as implementations of quantum factoring can easily be misinterpreted as a meaningful benchmark toward large-scale integer factorization, and we explain in this article why they are not.

For many years cryptographers have tracked and benchmarked progress in classical factorization and attempted extrapolations with an interest in estimating when RSA schemes with moduli of a given length may be broken using the number field sieve3,4. The extrapolations take into account estimates of computing power increase and algorithmic improvements.

This paper highlights why none of the current works in the literature on experimental implementations of quantum factoring serve the same purpose. In the absence of a breakthrough that demonstrates factoring can be meaningfully sped up without a fault-tolerant quantum computer, this sort of tracking of the size of numbers quantumly factored will only be meaningful after the implementation of several logical qubits.

One caveat and challenge with tracking and extrapolating is that once fault-tolerant quantum computers start factoring small numbers, a constant factor increase in available quantum resources brings a constant factor increase in the size of the number that can be factored (i.e. we go from being able to factor n-bit numbers to being able to factor (cn)-bit numbers for some \(c>1\) that depends on the factor of increase in time and memory) because Shor’s algorithm runs in expected polynomial time. On the other hand, a constant factor increase in classical computing resources only implies being able to factor numbers that are a few bits larger using the number field sieve (i.e. we go from being able to factor n-bit numbers to being able to factor \((n + o(n^{2/3}))\)-bit numbers). Given these quantum scalings, it will be much harder to reliably extrapolate the size of numbers that can be quantumly factored, and a relatively small change in computing resources or a relatively small algorithmic improvement can have a significant impact on the size of the number that can be quantumly factored. This is one reason why it is valuable to have post-quantum cryptography ready for wide-scale deployment before fault-tolerant quantum computers are available.

The Boolean satisfiability problem (SAT) asks whether there exists an assignment to the Boolean variables of a given propositional logic formula such that the formula evaluates to TRUE. This problem was the first that was proven to be NP-complete5,6. NP-complete problems are both NP-hard and in NP. Since no algorithms with polynomial runtime for NP-hard problems are known, solving NP-hard problems has long been considered to be intractable for real-world computers. Despite this result, coming from asymptotic analysis, modern SAT-solvers perform very well on solving large SAT instances originating from industry and academics, with formulas that have up to a million clauses7. At the moment of writing there exists no good general method or metric to predict if a given SAT instance is hard to solve. For practical applications it therefore makes sense to assess the performance of the solvers on the investigated instances by careful benchmarking instead of doing asymptotic analysis.

The approach considered in this work reduces factoring, a problem with a subexponential algorithm, to an NP-hard problem and then running (classical or quantum) solvers that have exponential runtime in the worst-case. At the surface, this obviously does not sound like a promising idea, as the quantum SAT solver must make up the exponential ground lost by translating the problem with subexponential algorithms to one where the best known algorithms are exponential. One might hope that good SAT solving heuristics for solving SAT on random or average-case instances could nevertheless have a practical impact on integer factorization.

The original goal of this project was to encode the RSA factoring challenges8 to SAT instances and see how well modern SAT solvers would perform on those instances. The smallest semi-prime of these challenges is RSA-100: a 100-digit or 330-bit number. This number was factored in a few days almost immediately after the challenge was posted9 in 1991, whereas the current record for factoring stands at factoring RSA-250: an 829-bit semi-prime10. The intention was to compare current state-of-the-art SAT solvers against the numerical results from 1991, but it turns out that even the smallest RSA semi-prime poses too big of a challenge for these solvers.

A more promising approach is to try to speed up the solution to some subroutine of the NFS, as is done in11. In particular, one could reduce some carefully chosen sub-problem solved within the number field sieve to SAT. The sub-problem should be chosen so that classically solving the SAT instance is roughly as costly as the usual approach to solving the sub-problem. In this case, any quantum speed-up for solving these SAT instances would lead to a faster implementation of the number field sieve. This approach is explored in12.

Contributions

This work provides a numerical analysis on the hardness of factoring numbers by solving the corresponding satisfiability problem, thereby confirming the folklore that factoring numbers does indeed give “hard” SAT instances. This is done by measuring the speed of the currently fastest SAT solver. We justify the choice of numerical analysis over theoretical asymptotic analysis by applying some common analysis tools from modern SAT solving theory and the observation that the tools provide no good prediction for the actual runtime. We extrapolate the numerical results to investigate the asymptotic behavior of the solver and compare the results with the asymptotics of factoring with numerical algorithms. Finally, the results are used to estimate an upper bound on the speedup that can be achieved on this specific problem using currently known quantum algorithms.

As a minor contribution, we developed a tool that can create smaller SAT instances for factoring (using long multiplication) than any other publicly available tool. This tool and scripts for generating semi-primes and reproducing the results of this paper have been made available online13.

SAT instances

An instance of the SAT problem is a formula in Boolean propositional logic. Every variable (x) can take the value TRUE or FALSE. An instance is said to be satisfiable if an assignment to the variables exists such that the overall formula evaluates to TRUE. Sometimes (as is the case when factoring via SAT) we are also interested in the values of the variables in the satisfying assignment itself. Formally this is no longer a decision problem, but we will sometimes be a bit informal in our language and discuss these as if they were decision problems.

This work considers CNF-SAT where all formulas are in conjunctive normal form (CNF): each formula must be a conjunction of disjunctions of literals. A literal is either a direct variable (x) or a negated variable (denoted \(\bar{x}\)), a disjunction of literals is called a clause. Further restricting each clause to exactly three literals would give the 3SAT problem. A satisfying assignment to CNF-SAT thus assigns a Boolean value to each variable such that at least one literal evaluates to TRUE in every clause. The CNF-SAT problem is equivalent to SAT14, in the sense that for each SAT instance an equisatisfiable CNF-SAT instance can easily be found with its size linear in the length of the original SAT instance. All tools we used for generating and solving SAT instances work with the DIMACS format which specifies formulas in CNF form.

A closely related problem is called CircuitSAT: given a Boolean circuit with a single output, is there an input such that the output is TRUE? One can translate any Boolean circuit into a Boolean formula: assign a variable to each input wire, then consider the logical operator corresponding to each gate (with a single output wire) in order. Each operator has a short CNF description, for example a NAND-gate (which forms a complete basis for Boolean formulas) with input wires x, y and output wire z has the corresponding formula \((x \vee z) \wedge (y \vee z) \wedge (\bar{x} \vee \bar{y} \vee \bar{z})\). Once the input wires are fixed to some value, there is only one possible value for the output wires such that the gate formula evaluates to TRUE. For example we fix can the input to \(x=\text {TRUE}\), \(y=\text {FALSE}\) by adding the clauses x and \(\bar{y}\). A SAT-solver can examine those five clauses and find that the only satisfying assignment sets \(z = \text{ TRUE }\). Combining gates to make a circuit is done by reusing output variables of earlier gates as input variables in later gates.

More interesting is to fix a value on the output variables of a circuit and ask the SAT-solver to find a satisfying assignment. For example adding the clause z to the NAND-gate gives three satisfying assignments: \(x \wedge \bar{y}\), \(\bar{x} \wedge y\), and \(\bar{x} \wedge \bar{y}\). In general a circuit might have zero or more satisfying assignments. Effectively the SAT-solver is finding preimages to the function described by the circuit. An immediate cryptanalytic application that springs to mind is finding preimages to secure hash functions: indeed this has been done with varying results15,16,17. More general cryptanalytic applications can be found throughout literature18 and occur in modern benchmarks7, although asymmetrical cryptographic primitives are rarely targeted.

This work examines circuits that encode the multiplication of two integers p and q. We fix the multiplication output bits of the circuit to the bit-values of the semi-prime N and ask the SAT-solver to find a satisfying assignment. Only two exist (trivial solutions are excluded by the problem encoding) those representing \(N=pq\) and \(N=qp\), so from the assignment one can read the factorization of N. For the remainder of this paper n represents the size of N in bits. We limit p and q similar to how the RSA cryptosystem limits its parameters: both need to be equally sized primes. We interpreted this last requirement to mean that their most significant bit may differ by at most one position.

Encoding

Despite the asymptotic worst-case exponential runtime associated with SAT instances, it is not trivial to generate “hard” SAT instances: instances where the solver runtime grows exponentially in the number of variables. For several problems (encoded as a SAT problem) it turns out that modern SAT solvers can solve many instances in short time in practice. Specialized tools such as ToughSat19 exist that can generate SAT instances that are hard on average, based on problems such as integer factorization.

Multiplying larger integers requires larger circuits, which leads to instances with more variables and clauses, which leads to longer solving times. However, there are many choices to make when computing multiplication in a circuit and each choice will lead to different encodings of the SAT instance and a different solver runtime. For SAT solvers in general it turns out that the details of the encoding of a problem (beyond metrics such as number of variables and clauses) can have a significant impact on the solver runtime. The first choice is to consider different multiplication algorithms: a simple one and a more complex encoding that in theory leads to smaller instances.

Long multiplication (or schoolbook multiplication) is computed by multiplying p by each digit (bit) of q and adding the shifted results. For multiplying two m-bit numbers (where \(m=n/2\)) this requires \(\Theta (m^2)\) bitwise multiplications and additions. The exact number of operations depends mainly on the circuit used for addition: our tool for generating instances13 minimizes the number of both variables and clauses by maximizing the number of full-adders used in the circuit. Counting the variables in the generated instances and applying regression reveals that the number of variables grows approximately as \(0.750n^2 + 0.496n - 2.05\) and similarly the number of clauses grows as \(4.25n^2 - 4.01n - 9.87\) with on average 3.31 literals per clause.

Karatsuba multiplication20 asymptotically improves upon long multiplication by a divide-and-conquer strategy and requires only \(\Theta (m^{\log _2 3})\) multiplications at the cost of requiring more additions. The instances we tested were generated by the ToughSat application19 and contain approximately \(2.59n^{\log _2 3} - 7.57n + 8.75\) variables and \(61.5n^{\log _2 3} - 170n - 386\) clauses with on average 6.77 literals per clause. Inspection of the generated instances reveals that the Karatsuba circuits were built from more complex gates, which explains why there are more literals per clause. It is likely that building the Karatsuba circuit with a similar gate set would increase the number of variables and clauses by another (constant) factor.

Asymptotically the Karatsuba algorithm is not the best known algorithm and is outperformed by for example Toom-Cook or FFT-multiplication. These methods introduce additional overhead that is especially significant for small instances, where it would result in larger SAT instances. Given that we also observed only a minor difference in the runtime of long multiplication and Karatsuba instances, we decided not to encode these more complex multiplication algorithms.

Hardware design provides alternative multiplication algorithms, which are often optimized to minimize latency and for various other physical constraints. There is no indication that these optimizations are related to optimizations that lead to smaller and/or easier SAT instances. In fact our adder encoded in the SAT instances minimizes the number of half-adders required, which gives the smallest number of variables and clauses and results in the fastest SAT solver times, but the resulting clauses encode a circuit that would give extremely high latency if built from physical components.

Since the multiplication circuit is the same for each semi-prime of the same bitlength there is an alternative strategy we can apply when we want to factor only one semi-prime out of a polynomial sized set. We encode the multiplication circuit once and then “fanout” the resulting wires to one circuit per semi-prime that checks if the output equals that semi-prime. Those results are combined with a large OR-gate, so that the entire instance evaluates to TRUE if the multiplication outcome is equal to any of the semi-primes. By inspecting which values were assigned on the circuit input wires by the solver we learn which of the semi-primes it actually factored. The idea behind this encoding is that if there is an easy semi-prime somewhere in the input, then the solver itself may detect this and focus on solving that instance. As long as we encode only polynomially many semi-primes in the instance, the total instance size will remain polynomial.

An alternative solution for factoring numbers with SAT is to encode the integer division circuit \(N / p = q + r\) and fixing the input value N and output remainder \(r=0\). The rationale for this encoding is that the solver would only have to assign values to the bits of p and can then deterministically evaluate the entire circuit and check if the remainder is zero. However, in practice this encoding leads to substantially larger SAT-instances and tests with various solvers indicate that solving such instances is significantly slower, so we did not investigate this encoding any further.

A more promising approach is to reduce some subroutine of the number field sieve (NFS) to SAT where there is little or no increase in complexity by map** to SAT, analogous to the approach taken by Bernstein, Biasse and Mosca11. In this case, even a small quantum speed-up will lead to a faster integer factorization algorithm. This approach is studied in detail in12.

Classical solvers

Modern SAT solvers come in two classes. Conflict-Driven Clause Learning (CDCL)21,22 combines conflict analysis with branch heuristics to systematically backtrack the search-space of an instance. Stochastic local search approaches such as employed by WalkSAT23 or simulated annealing combine randomized assignments with probabilistic updates to find assignments that minimize the number of clauses violated. We found that for the semi-prime instances CDCL solvers outperformed the local search solvers by an order of magnitude. The scope of this project is limited to the black-box analysis of publicly available SAT solvers. This means we will not investigate the internals of the solvers for analysis of the runtime, nor do we allow domain-specific knowledge to speed up solver times.

When considering the runtime T of an algorithm (either classical or quantum) we are most interested in the runtime as a function of the input size. In order to determine if one solver is faster than the other, we should always consider the total runtime. We measure the total runtime of the SAT solver including the runtime of the preprocessor. Technically the measurement should also include the time for generating the SAT instances, but this is negligible compared to the solver time. For many classical solvers the total runtime can be naturally partitioned into the time spent in pre-/post-processing (\(T_p\)) and the time spent solving (\(T_s\)): \(T(n) = T_p(n) + T_s(n)\) where n is the input size of the problem. Examples of this partitioning occur with the SAT preprocessor (\(T_p\)) and the SAT solver (\(T_s\)), the compiling (\(T_p\)) and running (\(T_s\)) of Shor’s algorithm or the creation of a Hamiltonian (\(T_p\)) and the execution of the adiabatic algorithm (\(T_s\)).

In order to properly analyze the runtime of any algorithm we need to consider T(n) and not just \(T_s(n)\), since an unbounded amount of preprocessing can find a solution and render \(T_s(n)\) to be trivial. We should also take care to set n to be the input size of the problem. Concretely this means we should let n be the size of the semi-prime and not the number of variables or clauses in our SAT instance. It is also important to analyse instance sizes larger than some lower bound (\(n \ge n_0\)), as the asymptotic behaviour is not visible for smaller sizes. For example the asymptotics of the MapleCOMSPS solver (discussed next) on integer factorization only become apparent at \(n_0 = 20\) bit semi-primes.

We tested the MapleCOMSPS24 SAT solver for the simple reason that at the time of running the benchmarks this was the fastest solver according to the SAT Competition 201625. We compiled and ran the solver with default settings, except for the random seed which was fixed for each call to the solver to ensure reproducibility of the results.

Another solver that we tested is CryptoMiniSat 526, because it has “Automatic detection of cryptographic [...] instances”27. One might consider this to be cheating by using domain-specific knowledge and therefore it should not be included in the benchmarks. CryptoMiniSat appears to focus on symmetric cryptography and appears to provide no speedup on public cryptography instances, which we confirmed during an initial round of benchmarking. We inspected the (partial) results and found that CryptoMiniSat 5 was consistently being outperformed by MapleCOMSPS. For this reason we did not further analyze this solver, but the results can be found in the Supplementary Material.

All measurements were performed on a ThinkPad laptop with a 64-bit Intel Core i5–4200M (Haswell) CPU running at 2.50 GHz. All measurements were executed sequentially and on a single core. Where applicable we use regression to fit a line to the data and the goodness-of-fit is quantified by the \(r^2\) parameter.

Results

Figure 1
figure 1

Runtime of MapleCOMSPS on factoring semi-primes.

Full size image

Usually when analyzing the runtime of a randomized algorithm we are interested in the expected runtime: the mean computed over the random bits. We do this by factoring the same number multiple times using a different PRNG-seed for the solver and average the runtime to compute the expected runtime numerically. We are interested in the asymptotics: the growth of the runtime as a function of the size of its input, so we group the semi-primes by their bitlength n (100 semi-primes per bitlength) and plot the mean runtime of solving five times. The results are given in Fig. 1a and are showing an exponential trend. The green line is fitted against the median runtime of all semi-primes of the same bitlength.

We repeated the same experiment for multiplication with the Karatsuba algorithm. The results are given in Fig. 1b: note that asymptotic runtime has improved somewhat over schoolbook multiplication at the cost of a larger constant. We conclude that changing the multiplication algorithm does not make factoring with SAT solvers efficient. Since the larger constant dominates the runtime at this small scale, we will consider schoolbook multiplication for the remainder of our experiments.

Figure 2
figure 2

Minimum runtime of MapleCOMSPS on factoring semi-primes using schoolbook multiplication.

Full size image

An alternative strategy for factoring is to run several solvers in parallel and wait for the first one to return a solution. We simulate this strategy by taking the minimum solver time of solving the same instance with the solver initialized with 100 different random seeds for 100 semi-primes per bitlength: the results are given in Fig. 2. Asymptotically the runtime became worse by employing this strategy. Note that this strategy does push down the constant by approximately \(2^{6.1}\). Since this is smaller than 100 it does not lead to a lower expected runtime on this small scale when we consider the total runtime of all parallel solvers.

We can also see in Fig. 2 that some semi-primes are significantly easier to solve than others with this strategy. Even if we only manage to factor some semi-primes that may be important to (for example) cryptography. For this method to be asymptotically efficient, it is required that the runtime is pushed down exponentially for more than just negligibly many cases. To see if it does we can inspect the distribution of the solver runtime given different seeds. Here we focus on three different semi-primes: the easiest, average and hardest semi-prime from the 100 semi-primes of 35 bits, where hardness is defined by the expected (mean) solve time computed over 360 seeds. The distribution for all other semi-primes can be generated at13.

Figure 3
figure 3

Histogram of the MapleCOMSPS runtime on factoring semi-primes using schoolbook multiplication.

Full size image

Although no strong conclusions should be drawn from the results in Fig. 3a, the distribution does suggest that running a few parallel solvers may lower the total runtime. To see if it may be considered efficient we again inspect the distribution but this time on a logarithmic scale: see Fig. 3b.

This data suggests that even if the method could push down the runtime significantly for any semi-prime, it only does so with negligible probability. Another way of interpreting this data is that employing parallel SAT solvers to factor a semi-prime does not appear to be better than employing a single solver.

Figure 4
figure 4

Runtime of MapleCOMSPS on factoring one of 100 semi-primes encoded in each instance using schoolbook multiplication.

Full size image

The last strategy we investigate is that of encoding multiple semi-primes into a single instance: for example an adversary may interested into breaking just one out of many cryptographic keys. We encoded 100 semi-primes per bitlength in each instance and solved it 100 times using different seeds. The results are given in Fig. 4. Note that whereas the vertical boxplots in previous plots show a distribution over different primes, here a distribution over different solver PRNG-seeds is shown. From the data we conclude that this strategy is less efficient than solving instances with a single semi-prime. From inspection of the solver solution we can see which semi-prime was factored (see13). This reveals that some semi-primes in the same instance are factored more often than others, suggesting that these are easier to factor by the solver, although we note that these are not “easy enough” to make the overall method efficient. The supplementary information contains further analysis of patterns in the SAT instances, but finds no pattern that can be exploited for significantly faster solver times.

Comparison to number-theoretical methods

One can put the above results in context by comparing the absolute runtime to that of other number-theoretical results. Using SageMath28 we measured the runtime of two approaches: factoring with the built-in factor function (Fig. 5a) and factoring by trial division (Fig. 5b).

Figure 5
figure 5

Runtime of factoring using numerical methods. No randomization was applied for obtaining these results.

Full size image

SageMath is able to factor almost all semi-primes up to a 100 bits in under 0.025 s. The tested semi-primes are so small that the asymptotic behavior of the underlying algorithm is not even visible yet, so there is no point in extrapolating these results. In fact the cross-over point where the NFS is faster than asymptotically slower methods such as the quadratic sieve and the elliptic-curve method is much larger than 100 bits, so that SageMath is not even using NFS to factor these small numbers. Instead, we refer to the literature to find that the best classical factoring algorithm (the general number field sieve29) runs in \(\exp \big ( ((64/9)^{1/3} + o(1)) (\ln N)^{1/3} (\ln N)^{2/3} \big ) = L_N[2/3, {(64/9)}^{1/3}]\) and this was indeed used to factor a 829-bit RSA modulus in approximately 2700 core-years10.

The timing of factoring using trial division is shown in Fig. 5b. The results reveal an exponential trend and with a much smaller constant than the SAT solver. On this small scale on which measurements were performed, trial division easily outperforms the SAT solvers. The asymptotic runtime of the methods are so close together that we cannot meaningfully extrapolate the results to find a cross-over point where the SAT solvers become faster than trial division. We therefore cannot rule out that factoring with classical SAT solvers is always slower than trial division.

Quantum solvers

State of the art classical factoring algorithms have super-polynomial expected runtime \(L_N[1/3, (64/9)^{1/3}]\)29, whereas Shor’s algorithm30 runs in expected polynomial time. This algorithm requires a fault-tolerant quantum computer and no scalable version has been implemented yet. Shor’s algorithm has profound practical implications for currently deployed public-key cryptography such as RSA and the timing of the factoring of 1024-bit, 2048-bit or even larger semi-primes is of great practical significance for both contemporary and future security systems31. Mitigations for future systems and current systems requiring long-term security are being researched by the field of post-quantum cryptography32,33,34.

An interesting notion of quantum computing has been proposed by Farhi et al.55.

A method called Variational Quantum Factoring (VQF)60. Exponential methods from computational algebraic geometry are used for preprocessing the instances without quantification of the (asymptotic or measured) runtime so that there is no indication of the efficiency of this preprocessing step. Although some statistics on the annealing process are provided for six semi-primes, not enough information is given for a meaningful assessment on the scalability of both the efficiency and effectiveness of this method.

Integer factorization has been implemented many times on the D-Wave 2000Q by similar strategies. While early experiments only factored four semi-primes61, later work62,63 has factored more numbers by reducing the required number of qubits through more preprocessing (in polylogarithmic time). Wang et al.63 claim \(O(n^2)\) annealing runtime without any justification; this unjustified claim seems incorrect, especially when considering the observation by Peng et al.62 that the rapidly decreasing accuracy limits the scalability of the method. None of these works presents convincing evidence that quantum annealing will find factors with significant likelihood in polynomial (or even sub-exponential) time.

A similar method was developed independently by Kieu64 and Yan et al.65. Their method translates factoring into an (NP-hard) optimization problem of minimizing \((N - pq)^2\) (or a similar expression), by encoding that directly in the problem Hamiltonian. Besides problems in translating the work to the Boolean logic required by the D-Wave machine66, the method has an exponential cost in energy in order to be efficient in time.

Discussion

SAT solvers are not known or believed to be able to factor semi-primes efficiently. Overall, even the fastest solver (MapleCOMSPS) has an exponential runtime in the size of the factors. Closer inspection of the solver runtime indicates that the solver is not able to detect any pattern in the SAT formulas that encode the factorization problem. Asymptotically the solver runtime appears to be comparable to that of trial division, but this advantage is almost completely negated by the overhead in the constant term. The performance of SAT solvers does not even come close to that of number-theoretical methods.

Of course if it were that easy RSA would be broken regularly by SAT solvers which is not the case. Furthermore, in practice it appears that SAT instances derived from integer factorization instances are hard SAT instances. Thus it would be especially surprising if a SAT solver could solve these instances with resources comparable to that of using the classical number field sieve (i.e. subexponential complexity).

Quantum SAT solvers are not expected to do much better. Published results from experiments on quantum hardware lack the details to conclude exactly how big of a quantum speedup can be practically achieved, but it certainly seems insufficient to make up for the gap introduced by switching from subexponential algorithms to (worst-case) exponential ones. Even when calculating a very optimistic quantum speedup to the current state-of-the-art classical solvers, these solvers are outperformed with orders of magnitude by (classical) number-theoretical factoring methods.

Our work explores the possibility of a quantum speedup more deeply and reinforces the folklore that reducing multiplication to SAT and then applying SAT solvers, classical or quantum, is not useful for factoring numbers of sizes relevant to cryptography.

Of course, one cannot rule out unexpected breakthroughs in quantum SAT solving or a wide range of other quantum or classical approaches to factoring semi-primes. However, it is important to distinguish the possibility of unexpected breakthroughs (especially those that contradict conventional wisdom or lack a plausible roadmap) from tracking progress of an existing hardware platform and of an algorithm that is pertinent for cryptographically relevant semi-primes (i.e. classical computers and the NFS). Once scalable fault-tolerant quantum computers capable of implementing Shor’s algorithm are available, a similar tracking would be very meaningful (with the caveat outlined in the introduction). In the meantime, it is important to track progress toward achieving scalable fault-tolerant quantum computers.

In other words, notwithstanding other scientific merits of these works, we are not aware of any evidence that any SAT-based quantum factoring results to date, including factorization by quantum annealing, are relevant milestones toward large-scale integer factorization or the demonstration of a speed-up over the best known classical algorithms for integer factorization.