Tags:Ising Machine, Natural Computation, Satisfiability and Stochastic Heuristics
Abstract:
Specialized combinatorial optimization solvers based on quadratic models, such as Ising and QUBO, exhibit a high degree of success in problems which map naturally to their formulation. For problems with higher order interactions, such as SAT, these quadratic dynamical solvers (QDS) have shown poor solution qualities due to excessive auxiliary variables and the resulting increase in energy landscape complexity. Thus, recently, a series of high order dynamical solver (HODS) models have been proposed for SAT and other problems. We show that such problem-agnostic HODS models still perform poorly on moderate to large problems, thus motivating the need to utilize SAT-specific heuristics. With this insight, our contributions can be summarized into three points. First, we demonstrate that existing make-only heuristics perform poorly on scale-free, industrial-like problems when integrated into HODS. This motivates us to utilize break counts as well. Second, we derive a relationship between make/break and the HODS formulation to efficiently recover break counts. Finally, we utilize this relationship to propose a new make/break heuristic and combine it with a state-of-the-art HODS which is projected to solve SAT problems several orders of magnitude faster than existing software solvers.
Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT