Efficient Solution of Boolean Satisfiability Problems with Digital MemComputing

TL;DR

This paper presents a novel digital memcomputing system that efficiently solves hard SAT problems with polynomial scalability, challenging the notion that such problems require exponential time in worst-case scenarios.

Contribution

Introduction of a memory-assisted physical system that demonstrates polynomially-bounded scalability in solving complex SAT instances through numerical integration.

Findings

Shows evidence of polynomial scalability in solving hard SAT instances.

Analytically proves efficient continuous-time solution without chaos or exponential energy.

Demonstrates robustness of the physical system's collective dynamics in guiding solutions.

Abstract

Boolean satisfiability is a propositional logic problem of interest in multiple fields, e.g., physics, mathematics, and computer science. Beyond a field of research, instances of the SAT problem, as it is known, require efficient solution methods in a variety of applications. It is the decision problem of determining whether a Boolean formula has a satisfying assignment, believed to require exponentially growing time for an algorithm to solve for the worst-case instances. Yet, the efficient solution of many classes of Boolean formulae eludes even the most successful algorithms, not only for the worst-case scenarios, but also for typical-case instances. Here, we introduce a memory-assisted physical system (a digital memcomputing machine) that, when its non-linear ordinary differential equations are integrated numerically, shows evidence for polynomially-bounded scalability while solving "hard" planted-solution instances of SAT, known to require exponential time to solve in the typical case for both complete and incomplete algorithms. Furthermore, we analytically demonstrate that the physical system can efficiently solve the SAT problem in continuous time, without the need to introduce chaos or an exponentially growing energy. The efficiency of the simulations is related to the collective dynamical properties of the original physical system that persist in the numerical integration to robustly guide the solution search even in the presence of numerical errors. We anticipate our results to broaden research directions in physics-inspired computing paradigms ranging from theory to application, from simulation to hardware implementation.