A high-performance analog Max-SAT solver and its application to Ramsey numbers
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$.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Exploring the Use of Shatter for AllSAT Through Ramsey-Type Problems
In the context of SAT solvers, Shatter is a popular tool for symmetry breaking on CNF formulas. Nevertheless, little has been said about its use in the context of AllSAT problems: problems where we are interested in list…
Vocal Bursts Type PredictionRamseyRL: A Framework for Intelligent Ramsey Number Counterexample Searching
The Ramsey number is the minimum number of nodes, $n = R(s, t)$, such that all undirected simple graphs of order $n$, contain a clique of order $s$, or an independent set of order $t$. This paper explores the application…
Reinforcement Learning (RL)A Novel Paradigm for Calculating Ramsey Number via Artificial Bee Colony Algorithm
The Ramsey number is of vital importance in Ramsey's theorem. This paper proposed a novel methodology for constructing Ramsey graphs about R(3,10), which uses Artificial Bee Colony optimization(ABC) to raise the lower bo…
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
Ramsey-good graphs are graphs that contain neither a clique of size $s$ nor an independent set of size $t$. We study doubly saturated Ramsey-good graphs, defined as Ramsey-good graphs in which the addition or removal of …
An Inverse-Ramsey Tax Rule
Traditional optimal commodity tax analysis, dating back to Ramsey (1927), prescribes that to maximize welfare one should impose higher taxes on goods with lower demand elasticities. Yet policy makers do not stress minimi…