Accelerating numerical simulation of continuous-time Boolean satisfiability solver using discrete gradient

Hiroshi Yamashita

doi:10.1016/j.cnsns.2021.105908

Return

Accelerating numerical simulation of continuous-time Boolean satisfiability solver using discrete gradient

2021-11-01

Hiroshi Yamashita *

Kazuyuki Aihara

Hideyuki Suzuki

DOI：10.1016/j.cnsns.2021.105908

Original

Save

View PDF

Abstract

En 中文

To explore the design of analog computing devices, modeling the problem-solving process as a continuous-time dynamical system is important. Ercsey-Ravasz and Toroczkai [Nature Physics 7, 966 (2011)] proposed such a model for solving the Boolean satisfiability (SAT) problem. This system consists of a gradient system that minimizes the potential function reduced from the SAT problem and a system for achieving a temporal variation of the po-tential function to avoid the problem of non-solution local minima. Although the ability of the system to find a solution to the SAT problem is demonstrated, its large simulation cost hinders theoretical research towards the physical realization and limits its utility on digital computers. This is due to the necessity of small time steps to maintain the numerical sta-bility of the simulation. In this study, we propose a fast and stable numerical simulation algorithm for this solver using the discrete gradient method to allow a larger time step. We also propose an adaptive time step control method for this system. The proposed algo-rithm achieves a faster simulation by a factor of approximately 100, compared to conven-tional methods. Although taking a large time step degrades the accuracy, we found that it does not necessarily degrade the performance as a SAT solver; this indicates the new util-ity of the discrete gradient apart from the conventional studies of numerical simulation algorithms that pursue accuracy as well as efficiency. (c) 2021 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY license ( http://creativecommons.org/licenses/by/4.0/ )

Keywords:

Boolean satisfiability problem

Continuous-time SAT solver

Discrete gradient

Adaptive step size

AI Summary

Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.