A high-performance analog Max-SAT solver and its application to Ramsey numbers

Abstract

We introduce a continuous-time analog solver for MaxSAT, a quintessential class of NP-hard discrete optimization problems, where the task is to find a truth assignment for a set of Boolean variables satisfying the maximum number of given logical constraints. We show that the scaling of an invariant of the solver's dynamics, the escape rate, as function of the number of unsatisfied clauses can predict the global optimum value, often well before reaching the corresponding state. We demonstrate the performance of the solver on hard MaxSAT competition problems. We then consider the two-color Ramsey number $R(m,m)$ problem, translate it to SAT, and apply our algorithm to the still unknown $R(5,5)$. We find edge colorings without monochromatic 5-cliques for complete graphs up to 42 vertices, while on 43 vertices we find colorings with only two monochromatic 5-cliques, the best coloring found so far, supporting the conjecture that $R(5,5)=43$.

arXiv comment33 pages, 13 figures. Version 2: added references, corrected SI tables

References in corpus (10)

• Practical approach to programmable analog circuits with memristors
• Network of Time-Multiplexed Optical Parametric Oscillators as a Coherent Ising Machine
• The random K-satisfiability problem: from an analytic solution to an efficient algorithm
• New Inference Rules for Max-SAT
• Optimization hardness as transient chaos in an analog approach to constraint satisfaction
• Reservoir computing with a single time-delay autonomous Boolean node
• Focused Local Search for Random 3-Satisfiability
• A 16-bit Coherent Ising Machine for One-Dimensional Ring and Cubic Graph Problems
• An event-based architecture for solving constraint satisfaction problems
• A Novel Approach to Complex Problems

Cited by in corpus (1)

• Spintronics-compatible approach to solving maximum satisfiability problems with probabilistic computing, invertible logic and parallel tempering