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.CP.2021.20
URN: urn:nbn:de:0030-drops-153110
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15311/
Go to the corresponding LIPIcs Volume Portal

Cherif, Mohamed Sami ; Habet, Djamal ; Terrioux, Cyril

Combining VSIDS and CHB Using Restarts in SAT

pdf-format:
LIPIcs-CP-2021-20.pdf (1 MB)

Abstract

Conflict Driven Clause Learning (CDCL) solvers are known to be efficient on structured instances and manage to solve ones with a large number of variables and clauses. An important component in such solvers is the branching heuristic which picks the next variable to branch on. In this paper, we evaluate different strategies which combine two state-of-the-art heuristics, namely the Variable State Independent Decaying Sum (VSIDS) and the Conflict History-Based (CHB) branching heuristic. These strategies take advantage of the restart mechanism, which helps to deal with the heavy-tailed phenomena in SAT, to switch between these heuristics thus ensuring a better and more diverse exploration of the search space. Our experimental evaluation shows that combining VSIDS and CHB using restarts achieves competitive results and even significantly outperforms both heuristics for some chosen strategies.

BibTeX - Entry

@InProceedings{cherif_et_al:LIPIcs.CP.2021.20,
  author =	{Cherif, Mohamed Sami and Habet, Djamal and Terrioux, Cyril},
  title =	{{Combining VSIDS and CHB Using Restarts in SAT}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/15311},
  URN =		{urn:nbn:de:0030-drops-153110},
  doi =		{10.4230/LIPIcs.CP.2021.20},
  annote =	{Keywords: Satisfiability, Branching Heuristic, Restarts}
}

Keywords: Satisfiability, Branching Heuristic, Restarts
Collection: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)
Issue Date: 2021
Date of publication: 15.10.2021

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