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

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/ )

Automated summary

The study explores the design of analog computing devices and proposes a model for solving the SAT problem. Despite high simulation costs, a new simulation algorithm allows for faster solutions.