License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.25
URN: urn:nbn:de:0030-drops-184871
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18487/
Go to the corresponding LIPIcs Volume Portal

Sharma, Anshujit ; Burns, Matthew ; Huang, Michael C.

Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT

pdf-format:
LIPIcs-SAT-2023-25.pdf (4 MB)

Abstract

Dynamical solvers for combinatorial optimization are usually based on 2superscript{nd} degree polynomial interactions, such as the Ising model. These exhibit high success for problems that map naturally to their formulation. However, SAT requires higher degree of interactions. As such, these quadratic dynamical solvers (QDS) have shown poor solution quality due to excessive auxiliary variables and the resulting increase in search-space complexity. Thus recently, a series of cubic dynamical solver (CDS) models have been proposed for SAT and other problems. We show that such problem-agnostic CDS 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 CDS. This motivates us to utilize break counts as well. Second, we derive a relationship between make/break and the CDS 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 CDS which is projected to solve SAT problems several orders of magnitude faster than existing software solvers.

BibTeX - Entry

@InProceedings{sharma_et_al:LIPIcs.SAT.2023.25,
  author =	{Sharma, Anshujit and Burns, Matthew and Huang, Michael C.},
  title =	{{Combining Cubic Dynamical Solvers with Make/Break Heuristics to Solve SAT}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{25:1--25:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18487},
  URN =		{urn:nbn:de:0030-drops-184871},
  doi =		{10.4230/LIPIcs.SAT.2023.25},
  annote =	{Keywords: Satisfiability, Ising machines, Stochastic Heuristics, Natural Computation}
}

Keywords: Satisfiability, Ising machines, Stochastic Heuristics, Natural Computation
Collection: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Issue Date: 2023
Date of publication: 09.08.2023
Supplementary Material: InteractiveResource (Experimental data, benchmarks and solver infrastructure): https://ising.ece.rochester.edu/sat

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI