Coherent SAT solvers: a tutorial
Sam Reifenstein, Timothée Leleu, Timothy P. McKenna, Marc Jankowski, Myoung‐Gyun Suh, Edwin Ng, Farad Khoyratee, Zoltán Toroczkai, Y. Yamamoto
Abstract
The coherent Ising machine (CIM) is designed to solve the NP-hard Ising problem quickly and energy efficiently. Boolean satisfiability (SAT) and maximum satisfiability (Max-SAT) are classes of NP-complete and NP-hard problems that are equally important and more practically relevant combinatorial optimization problems. Many approaches exist for solving Boolean SAT, such as quantum annealing and classical stochastic local search (SLS) solvers; however, they all are expected to require many steps to solve hard SAT problems and, thus, require large amounts of time and energy. In addition, a SAT problem can be converted into an Ising problem and solved by an Ising machine; however, we have found that this approach has drawbacks. As well as reviewing existing approaches to solving the SAT problem, we have extended the CIM algorithm and architecture to solve SAT and Max-SAT problems directly. This new technique is termed a coherent SAT solver (CSS). We have studied three implementations of the CSS, all-optical, hybrid optical–digital and all digital (cyber-CSS), and have compared the time-to-solution and energy-to-solution of three machines. The cyber-CSS, which is already implemented using a graphics processing unit (GPU), demonstrates competitive performance against existing SLS solvers such as probSAT. The CSS is also compared with another continuous-time SAT solver known as the CTDS, and the scaling behavior is evaluated for random 3-SAT problems. The hybrid optical–digital CSS is a more performant and practical machine that can be realized in a short term. Finally, the all-optical CSS promises the best energy-to-solution cost; however various technical challenges in nonlinear optics await us in order to build this machine.