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 solving combinatorial 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 boolean satisfiability (SAT) problems. We demonstrate that, in the case of 3-SAT, a basic architecture fails to produce meaningful acceleration, largely due 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. Using numerical simulations, we show that such an "Augmented" Ising Machine for SAT is projected to outperform state-of-the-art software-based, GPU-based and conventional hardware SAT solvers by orders of magnitude.
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 solving combinatorial 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 boolean satisfiability (SAT) problems. We demonstrate that, in the case of 3-SAT, a basic architecture fails to produce meaningful acceleration, largely due 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. Using numerical simulations, we show that such an "Augmented" Ising Machine for SAT is projected to outperform state-of-the-art software-based, GPU-based and conventional hardware SAT solvers by orders of magnitude.
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.
Ising Machines are emerging hardware architectures that efficiently solve NP-Hard combinatorial optimization problems. Generally, combinatorial problems are transformed into quadratic unconstrained binary optimization (QUBO) form, but this transformation often complicates the solution landscape, degrading performance, especially for multi-state problems. To address this challenge, we model spin interactions as generalized boolean logic function to significantly reduce the exploration space. We demonstrate the effectiveness of our approach on graph coloring problem using probabilistic Ising solvers, achieving similar accuracy compared to state-of-the-art heuristics and machine learning algorithms. It also shows significant improvement over state-of-the-art QUBO-based Ising solvers, including probabilistic Ising and simulated bifurcation machines. We also design 1024-neuron all-to-all connected probabilistic Ising accelerator on FPGA with the proposed approach that shows ~10000x performance acceleration compared to GPU-based Tabucol heuristics and reducing physical neurons by 1.5-4x over baseline Ising frameworks. Thus, this work establishes superior efficiency, scalability and solution quality for multi-state optimization problems.
Ising machines are specialized devices designed to efficiently solve combinatorial optimization problems. Among such problems, Boolean Satisfiability (SAT) is particularly relevant in industrial applications. To solve SAT problems using Ising machines, it is crucial to incorporate higher-order interactions. However, in analog Ising machines, interactions of different orders scale unevenly with the continuous spin amplitudes, introducing imbalances that can significantly degrade performance. Here we present a numerical comparison of methods to mitigate these imbalances, evaluating time-to-solution and success rate on uniform random 3-SAT and 4-SAT instances. Our results show that the most effective approach employs spin interactions that are proportional to the signs of spins, rather than their continuous amplitudes. We further demonstrate that smooth approximations of this method make it compatible with analog hardware. These findings underscore the central role of spin-sign-based interactions in enabling robust and scalable analog Ising machine dynamics. Ising machines (IMs) offer promising solutions for combinatorial optimization problems yet face challenges with imbalances in higher-order interactions when applied to Boolean Satisfiability (SAT) tasks. Here, the authors demonstrate that employing spin-sign-based interactions effectively mitigates these imbalances, enhancing performance and compatibility with analog hardware, thus advancing robust and scalable IM dynamics.
Abstract Ising Machines are emerging hardware architectures that efficiently solve NP-hard combinatorial optimization problems. Generally, combinatorial problems are transformed into quadratic unconstrained binary optimization (QUBO) form, but this transformation often complicates the solution landscape, degrading performance, especially for multi-state problems. To address this challenge, we model spin interactions as generalized boolean logic function to significantly reduce the exploration space. We demonstrate the effectiveness of our approach on graph coloring problem using probabilistic Ising solvers, achieving similar accuracy compared to state-of-the-art heuristics and machine learning algorithms. It also shows significant improvement over state-of-the-art QUBO-based Ising solvers, including probabilistic Ising and simulated bifurcation machines. We also design 1024-neuron all-to-all connected probabilistic Ising accelerator on FPGA with the proposed approach that shows ∼ ~ 10000 × × performance acceleration compared to GPU-based Tabucol heuristics and reducing physical neurons by 1.5 − − 4 × × over baseline Ising frameworks. Thus, this work establishes superior efficiency, scalability and solution quality for multi-state optimization problems.
Quadratic Unconstrained Binary Optimization (QUBO) problems are NP-hard problems and many real-world problems can be formulated as QUBO. Currently there are no algorithms known that can solve arbitrary instances of NP-hard problems efficiently. Therefore special-purpose hardware such as Digital Annealer, other Ising machines, as well as quantum annealers might lead to benefits in solving such problems. We study a particularly hard class of problems which can be formulated as QUBOs, namely Boolean satisfiability (SAT) problems, and specifically 3-SAT. One intriguing aspect about 3-SAT problems is that there are different transformations from 3-SAT to QUBO. We study the transformations' influence on the problem solution, using Digital Annealer as a special-purpose solver. Besides well-known transformations we investigate a novel in this context not yet discussed transformation, using less auxiliary variables and leading to very good performance. Using exact diagonalization, we explain the differences in performance originating from the different transformations. We envision that this knowledge allows for specifically engineering transformations that improve a solvers capacity to find high quality solutions. Furthermore, we show that the Digital Annealer outperforms a quantum annealer in solving hard 3-SAT instances.
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.