Augmenting an electronic Ising machine to effectively solve boolean satisfiability
Abstract 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 optimiz...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Nature Portfolio
2023-12-01
|
| Series: | Scientific Reports |
| Online Access: | https://doi.org/10.1038/s41598-023-49966-6 |
| _version_ | 1797376998624985088 |
|---|---|
| author | Anshujit Sharma Matthew Burns Andrew Hahn Michael Huang |
| author_facet | Anshujit Sharma Matthew Burns Andrew Hahn Michael Huang |
| author_sort | Anshujit Sharma |
| collection | DOAJ |
| description | Abstract 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. |
| first_indexed | 2024-03-08T19:46:38Z |
| format | Article |
| id | doaj.art-b8ac15ec1b304ebab597804ea34cb99f |
| institution | Directory Open Access Journal |
| issn | 2045-2322 |
| language | English |
| last_indexed | 2024-03-08T19:46:38Z |
| publishDate | 2023-12-01 |
| publisher | Nature Portfolio |
| record_format | Article |
| series | Scientific Reports |
| spelling | doaj.art-b8ac15ec1b304ebab597804ea34cb99f2023-12-24T12:19:01ZengNature PortfolioScientific Reports2045-23222023-12-0113111010.1038/s41598-023-49966-6Augmenting an electronic Ising machine to effectively solve boolean satisfiabilityAnshujit Sharma0Matthew Burns1Andrew Hahn2Michael Huang3Department of Electrical and Computer Engineering, University of RochesterDepartment of Electrical and Computer Engineering, University of RochesterDepartment of Electrical and Computer Engineering, University of RochesterDepartment of Electrical and Computer Engineering, University of RochesterAbstract 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.https://doi.org/10.1038/s41598-023-49966-6 |
| spellingShingle | Anshujit Sharma Matthew Burns Andrew Hahn Michael Huang Augmenting an electronic Ising machine to effectively solve boolean satisfiability Scientific Reports |
| title | Augmenting an electronic Ising machine to effectively solve boolean satisfiability |
| title_full | Augmenting an electronic Ising machine to effectively solve boolean satisfiability |
| title_fullStr | Augmenting an electronic Ising machine to effectively solve boolean satisfiability |
| title_full_unstemmed | Augmenting an electronic Ising machine to effectively solve boolean satisfiability |
| title_short | Augmenting an electronic Ising machine to effectively solve boolean satisfiability |
| title_sort | augmenting an electronic ising machine to effectively solve boolean satisfiability |
| url | https://doi.org/10.1038/s41598-023-49966-6 |
| work_keys_str_mv | AT anshujitsharma augmentinganelectronicisingmachinetoeffectivelysolvebooleansatisfiability AT matthewburns augmentinganelectronicisingmachinetoeffectivelysolvebooleansatisfiability AT andrewhahn augmentinganelectronicisingmachinetoeffectivelysolvebooleansatisfiability AT michaelhuang augmentinganelectronicisingmachinetoeffectivelysolvebooleansatisfiability |