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

Semenov, Alexander ; Chivilikhin, Daniil ; Pavlenko, Artem ; Otpuschennikov, Ilya ; Ulyantsev, Vladimir ; Ignatiev, Alexey

Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms

pdf-format:
LIPIcs-CP-2021-47.pdf (1.0 MB)

Abstract

Propositional satisfiability (SAT) solvers are deemed to be among the most efficient reasoners, which have been successfully used in a wide range of practical applications. As this contrasts the well-known NP-completeness of SAT, a number of attempts have been made in the recent past to assess the hardness of propositional formulas in conjunctive normal form (CNF). The present paper proposes a CNF formula hardness measure which is close in conceptual meaning to the one based on Backdoor set notion: in both cases some subset B of variables in a CNF formula is used to define the hardness of the formula w.r.t. this set. In contrast to the backdoor measure, the new measure does not demand the polynomial decidability of CNF formulas obtained when substituting assignments of variables from B to the original formula. To estimate this measure the paper suggests an adaptive (ε,δ)-approximation probabilistic algorithm. The problem of looking for the subset of variables which provides the minimal hardness value is reduced to optimization of a pseudo-Boolean black-box function. We apply evolutionary algorithms to this problem and demonstrate applicability of proposed notions and techniques to tests from several families of unsatisfiable CNF formulas.

BibTeX - Entry

@InProceedings{semenov_et_al:LIPIcs.CP.2021.47,
  author =	{Semenov, Alexander and Chivilikhin, Daniil and Pavlenko, Artem and Otpuschennikov, Ilya and Ulyantsev, Vladimir and Ignatiev, Alexey},
  title =	{{Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{47:1--47:18},
  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/15338},
  URN =		{urn:nbn:de:0030-drops-153381},
  doi =		{10.4230/LIPIcs.CP.2021.47},
  annote =	{Keywords: SAT solving, Boolean formula hardness, Backdoors, Evolutionary algorithms}
}

Keywords: SAT solving, Boolean formula hardness, Backdoors, Evolutionary algorithms
Collection: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)
Issue Date: 2021
Date of publication: 15.10.2021
Supplementary Material: Software (Source Code): https://github.com/ctlab/EvoGuess

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