Augmented Electronic Ising Machine as an Effective SAT Solver

• URL: http://arxiv.org/abs/2305.01623v1
• Date: Mon, 1 May 2023 02:28:42 GMT
• Title: Augmented Electronic Ising Machine as an Effective SAT Solver
• Authors: Anshujit Sharma, Matthew Burns, Andrew Hahn, and Michael Huang
• Abstract summary: We show that 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.
• Score: 0.6999740786886535
• License: http://creativecommons.org/licenses/by/4.0/
• 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 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.

Related papers

• TRIP: Trainable Region-of-Interest Prediction for Hardware-Efficient Neuromorphic Processing on Event-based Vision [33.803108353747305]
  Trainable Region-of-Interest Prediction (TRIP) is a framework for event-based vision processing on a neuromorphic processor. TRIP exploits sparse events' inherent low information density to reduce the overhead of ROI prediction. Our solution requires 46x less computation than the state-of-the-art while achieving higher accuracy.
  arXiv  Detail & Related papers  (2024-06-25T12:04:51Z)
• All-to-all reconfigurability with sparse and higher-order Ising machines [0.0]
  We introduce a multiplexed architecture that emulates all-to-all network functionality. We show that running the adaptive parallel tempering algorithm demonstrates competitive algorithmic and prefactor advantages. scaled magnetic versions of p-bit IMs could lead to orders of magnitude improvements over the state of the art for generic optimization.
  arXiv  Detail & Related papers  (2023-11-21T20:27:02Z)
• Qubit efficient quantum algorithms for the vehicle routing problem on NISQ processors [48.68474702382697]
  Vehicle routing problem with time windows (VRPTW) is a common optimization problem faced within the logistics industry. In this work, we explore the use of a previously-introduced qubit encoding scheme to reduce the number of binary variables.
  arXiv  Detail & Related papers  (2023-06-14T13:44:35Z)
• Computability of Optimizers [71.84486326350338]
  We will show that in various situations the is unattainable on Turing machines and consequently on digital computers. We prove such results for a variety of well-known problems from very different areas, including artificial intelligence, financial mathematics, and information theory.
  arXiv  Detail & Related papers  (2023-01-15T17:41:41Z)
• Efficient Optimization with Higher-Order Ising Machines [5.697064222465131]
  We show that higher-order Ising machines can solve satisfiability problems more resource-efficiently than traditional second-order Ising machines. Our results improve the current state-of-the-art for Ising machines.
  arXiv  Detail & Related papers  (2022-12-07T03:18:05Z)
• MAPLE-X: Latency Prediction with Explicit Microprocessor Prior Knowledge [87.41163540910854]
  Deep neural network (DNN) latency characterization is a time-consuming process. We propose MAPLE-X which extends MAPLE by incorporating explicit prior knowledge of hardware devices and DNN architecture latency.
  arXiv  Detail & Related papers  (2022-05-25T11:08:20Z)
• Adiabatic Quantum Computing for Multi Object Tracking [170.8716555363907]
  Multi-Object Tracking (MOT) is most often approached in the tracking-by-detection paradigm, where object detections are associated through time. As these optimization problems are often NP-hard, they can only be solved exactly for small instances on current hardware. We show that our approach is competitive compared with state-of-the-art optimization-based approaches, even when using of-the-shelf integer programming solvers.
  arXiv  Detail & Related papers  (2022-02-17T18:59:20Z)
• Scaling Quantum Approximate Optimization on Near-term Hardware [49.94954584453379]
  We quantify scaling of the expected resource requirements by optimized circuits for hardware architectures with varying levels of connectivity. We show the number of measurements, and hence total time to synthesizing solution, grows exponentially in problem size and problem graph degree. These problems may be alleviated by increasing hardware connectivity or by recently proposed modifications to the QAOA that achieve higher performance with fewer circuit layers.
  arXiv  Detail & Related papers  (2022-01-06T21:02:30Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• 3-Regular 3-XORSAT Planted Solutions Benchmark of Classical and Quantum Heuristic Optimizers [0.30586855806896046]
  Special-purpose hardware has emerged as an option to tackle specific computing-intensive challenges. These platforms come in many different flavors, from highly-efficient hardware implementations on digital-logic to proposals of analog hardware implementing new algorithms. In this work, we use a mapping of a specific class of linear equations whose solutions can be found efficiently, to benchmark several of these different approaches.
  arXiv  Detail & Related papers  (2021-03-15T15:40:00Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.