© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

Advances in Optics and Photonics

Coherent SAT solvers: a tutorial

Sam Reifenstein, Timothee G. Leleu, Timothy P. McKenna, Marc Jankowski, Myoung‐Gyun Suh, Edwin Ng, Farad Khoyratee, Zoltán Toroczkai, Y. Yamamoto

Published Mar 22, 2023• 17 citations

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.

DOI: 10.1364/aop.475823

Related papers

CITS: Coherent Ising Tree Search Algorithm Towards Solving Combinatorial Optimization Problems

Yunuo Cen, Debasis Das, Xuanyao Fong

Simulated annealing (SA) attracts more attention among classical heuristic algorithms because the solution of the combinatorial optimization problem can be naturally mapped to the ground state of the Ising Hamiltonian. However, in practical implementation, the annealing process cannot be arbitrarily slow and hence, it may deviate from the expected stationary Boltzmann distribution and become trapped in a local energy minimum. To overcome this problem, this paper proposes a heuristic search algorithm by expanding search space from a Markov chain to a recursive depth limited tree based on SA, where the parent and child nodes represent the current and future spin states. At each iteration, the algorithm will select the best near-optimal solution within the feasible search space by exploring along the tree in the sense of `look ahead'. Furthermore, motivated by coherent Ising machine (CIM), we relax the discrete representation of spin states to continuous representation with a regularization term and utilize the reduced dynamics of the oscillators to explore the surrounding neighborhood of the selected tree nodes. We tested our algorithm on a representative NP-hard problem (MAX-CUT) to illustrate the effectiveness of this algorithm compared to semi-definite programming (SDP), SA, and simulated CIM. Our results show that above the primal heuristics SA and CIM, our high-level tree search strategy is able to provide solutions within fewer epochs for Ising formulated NP-optimization problems.

arXiv:2203.09926•Mar 9, 2022•0 citations

Augmented Electronic Ising Machine as an Effective SAT Solver

Anshujit Sharma, Burns, Matthew, Andrew Warren Hahn +1 more

With the slowdown of improvement in conventional von Neumann systems, increasing attention is paid to novel paradigms such as Ising machines. They have very different approach to NP-complete optimization problems. Ising machines have shown great potential in solving binary optimization problems like MaxCut. In this paper, we present an analysis of these systems in satisfiability (SAT) problems. We demonstrate that, in the case of 3-SAT, a basic architecture fails to produce meaningful acceleration, thanks in no small part to the relentless progress made in conventional SAT solvers. Nevertheless, careful analysis attributes part of the failure to the lack of two important components: cubic interactions and efficient randomization heuristics. To overcome these limitations, we add proper architectural support for cubic interaction on a state-of-the-art Ising machine. More importantly, we propose a novel semantic-aware annealing schedule that makes the search-space navigation much more efficient than existing annealing heuristics. With experimental analyses, we show that such an Augmented Ising Machine for SAT (AIMS), outperforms state-of-the-art software-based, GPU-based and conventional hardware SAT solvers by orders of magnitude. We also demonstrate AIMS to be relatively robust against device variation and noise.

arXiv:2305.01623•May 1, 2023•1 citation

A coherent Ising machine with quantum measurement and feedback control

Yoshitaka Haribara, Y. Yamamoto, Ken‐ichi Kawarabayashi +1 more

Combinatorial optimization problems are computationally hard in general, but they are ubiquitous in our modern life. A coherent Ising machine (CIM) based on a multiple-pulse degenerate optical parametric oscillator (DOPO) is an alternative approach to solve these problems by a specialized physical computing system. To evaluate its potential performance, computational experiments are performed on maximum cut (MAX-CUT) problems against traditional algorithms such as semidefinite programming relaxation of Goemans-Williamson and simulated annealing by Kirkpatrick, et al. The numerical results empirically suggest that the almost constant computation time is required to obtain the reasonably accurate solutions of MAX-CUT problems on a CIM with the number of vertices up to $2 \times 10^4$ and the number of edges up to $10^8$.

•Jan 28, 2015•5 citations

Quantum Annealing and the Satisfiability Problem

Kristen L. Pudenz, Tallant Gregory S., Todd R. Belote +1 more

The utility of satisfiability (SAT) as an application focused hard computational problem is well established. We explore the potential of quantum annealing to enhance classical SAT solving, especially where sampling from the space of all possible solutions is of interest. We address the formulation of SAT problems to make them suitable for commercial quantum annealers, practical concerns in their implementation, and how the performance of the resulting quantum solver compares to and complements classical SAT solvers.

Advances in parallel computing•Jan 1, 2017•0 citations

A Comparative Study of Coherent Ising Machine Architectures Through a Unified Simulation Model

Vidisha Singhal, Peter A. Bermel

Coherent Ising Machines (CIMs) have emerged as promising hardware solvers for NP-hard combinatorial optimization problems, potentially offering energy-efficiency, accuracy, speed, and scalability. These problems span applications including scheduling, routing, resource allocation, and machine learning. Spin amplitude inhomogeneity (an artifact of its analog nature) can hinder CIM convergence to the ground state. Several CIM modifications have been proposed to address this issue. However, no prior work has systematically compared the performance of these concepts. This paper presents the first side-by-side evaluation of six promising CIM architectures using a unified simulation model. We develop stochastic differential equations, find optimal hyperparameters via Bayesian optimization per problem-architecture pair, and assess the performance on multiple metrics using MaxCut instances from the Gset and BiqMac datasets. CIM-SNN outperforms the rest on most metrics, with a 54.21% average success probability (SP) improvement and 1.36× less time-to-solution (TTS) at 96% GS energy compared to the Standard CIM on BiqMac graphs. Other CIMs show some advantages on certain Gset graphs. CIM-QA is usually the worst-performing, with an 18.55% average SP loss and a 1.30× higher TTS at 96% GS compared to the Standard CIM on BiqMac graphs. CIM-SNN demonstrates the greatest noise robustness and promise for further tuning via a linear pump schedule. CIM-QA benefits from high noise levels. This study makes two key contributions: (1) identifying promising CIM architectures to guide targeted research and accelerate practical adoption, and (2) providing a unified framework for evaluating future architectural modifications against existing ones.

IEEE Access•Jan 1, 2025•0 citations

Quantum Annealing and the Satisfiability Problem

Kristen L. Pudenz, Greg S. Tallant, Todd R. Belote +1 more

The utility of satisfiability (SAT) as an application focused hard computational problem is well established. We explore the potential of quantum annealing to enhance classical SAT solving, especially where sampling from the space of all possible solutions is of interest. We address the formulation of SAT problems to make them suitable for commercial quantum annealers, practical concerns in their implementation, and how the performance of the resulting quantum solver compares to and complements classical SAT solvers.

arXiv:1612.07258•Dec 21, 2016•5 citations

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.

Simulated annealing (SA) attracts more attention among classical heuristic algorithms because the solution of the combinatorial optimization problem can be naturally mapped to the ground state of the Ising Hamiltonian. However, in practical implementation, the annealing process cannot be arbitrarily slow and hence, it may deviate from the expected stationary Boltzmann distribution and become trapped in a local energy minimum. To overcome this problem, this paper proposes a heuristic search algorithm by expanding search space from a Markov chain to a recursive depth limited tree based on SA, where the parent and child nodes represent the current and future spin states. At each iteration, the algorithm will select the best near-optimal solution within the feasible search space by exploring along the tree in the sense of `look ahead'. Furthermore, motivated by coherent Ising machine (CIM), we relax the discrete representation of spin states to continuous representation with a regularization term and utilize the reduced dynamics of the oscillators to explore the surrounding neighborhood of the selected tree nodes. We tested our algorithm on a representative NP-hard problem (MAX-CUT) to illustrate the effectiveness of this algorithm compared to semi-definite programming (SDP), SA, and simulated CIM. Our results show that above the primal heuristics SA and CIM, our high-level tree search strategy is able to provide solutions within fewer epochs for Ising formulated NP-optimization problems.

With the slowdown of improvement in conventional von Neumann systems, increasing attention is paid to novel paradigms such as Ising machines. They have very different approach to NP-complete optimization problems. Ising machines have shown great potential in solving binary optimization problems like MaxCut. In this paper, we present an analysis of these systems in satisfiability (SAT) problems. We demonstrate that, in the case of 3-SAT, a basic architecture fails to produce meaningful acceleration, thanks in no small part to the relentless progress made in conventional SAT solvers. Nevertheless, careful analysis attributes part of the failure to the lack of two important components: cubic interactions and efficient randomization heuristics. To overcome these limitations, we add proper architectural support for cubic interaction on a state-of-the-art Ising machine. More importantly, we propose a novel semantic-aware annealing schedule that makes the search-space navigation much more efficient than existing annealing heuristics. With experimental analyses, we show that such an Augmented Ising Machine for SAT (AIMS), outperforms state-of-the-art software-based, GPU-based and conventional hardware SAT solvers by orders of magnitude. We also demonstrate AIMS to be relatively robust against device variation and noise.

Combinatorial optimization problems are computationally hard in general, but they are ubiquitous in our modern life. A coherent Ising machine (CIM) based on a multiple-pulse degenerate optical parametric oscillator (DOPO) is an alternative approach to solve these problems by a specialized physical computing system. To evaluate its potential performance, computational experiments are performed on maximum cut (MAX-CUT) problems against traditional algorithms such as semidefinite programming relaxation of Goemans-Williamson and simulated annealing by Kirkpatrick, et al. The numerical results empirically suggest that the almost constant computation time is required to obtain the reasonably accurate solutions of MAX-CUT problems on a CIM with the number of vertices up to

2 \times 10^4

and the number of edges up to

10^8

.

The utility of satisfiability (SAT) as an application focused hard computational problem is well established. We explore the potential of quantum annealing to enhance classical SAT solving, especially where sampling from the space of all possible solutions is of interest. We address the formulation of SAT problems to make them suitable for commercial quantum annealers, practical concerns in their implementation, and how the performance of the resulting quantum solver compares to and complements classical SAT solvers.

Coherent Ising Machines (CIMs) have emerged as promising hardware solvers for NP-hard combinatorial optimization problems, potentially offering energy-efficiency, accuracy, speed, and scalability. These problems span applications including scheduling, routing, resource allocation, and machine learning. Spin amplitude inhomogeneity (an artifact of its analog nature) can hinder CIM convergence to the ground state. Several CIM modifications have been proposed to address this issue. However, no prior work has systematically compared the performance of these concepts. This paper presents the first side-by-side evaluation of six promising CIM architectures using a unified simulation model. We develop stochastic differential equations, find optimal hyperparameters via Bayesian optimization per problem-architecture pair, and assess the performance on multiple metrics using MaxCut instances from the Gset and BiqMac datasets. CIM-SNN outperforms the rest on most metrics, with a 54.21% average success probability (SP) improvement and 1.36× less time-to-solution (TTS) at 96% GS energy compared to the Standard CIM on BiqMac graphs. Other CIMs show some advantages on certain Gset graphs. CIM-QA is usually the worst-performing, with an 18.55% average SP loss and a 1.30× higher TTS at 96% GS compared to the Standard CIM on BiqMac graphs. CIM-SNN demonstrates the greatest noise robustness and promise for further tuning via a linear pump schedule. CIM-QA benefits from high noise levels. This study makes two key contributions: (1) identifying promising CIM architectures to guide targeted research and accelerate practical adoption, and (2) providing a unified framework for evaluating future architectural modifications against existing ones.

The utility of satisfiability (SAT) as an application focused hard computational problem is well established. We explore the potential of quantum annealing to enhance classical SAT solving, especially where sampling from the space of all possible solutions is of interest. We address the formulation of SAT problems to make them suitable for commercial quantum annealers, practical concerns in their implementation, and how the performance of the resulting quantum solver compares to and complements classical SAT solvers.