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.2022.3
URN: urn:nbn:de:0030-drops-166775
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16677/
Go to the corresponding LIPIcs Volume Portal

Garzón, Iván ; Mesejo, Pablo ; Giráldez-Cru, Jesús

On the Performance of Deep Generative Models of Realistic SAT Instances

pdf-format:
LIPIcs-SAT-2022-3.pdf (3 MB)

Abstract

Generating realistic random SAT instances - random SAT formulas with computational characteristics similar to the ones of application SAT benchmarks - is a challenging problem in order to understand the success of modern SAT solvers solving this kind of problems. Traditional approaches are based on probabilistic models, where a probability distribution characterizes the occurrences of variables into clauses in order to mimic a certain feature exhibited in most application formulas (e.g., community structure), but they may be unable to reproduce others. Alternatively, deep generative models have been recently proposed to address this problem. The goal of these models is to learn the whole structure of the formula without focusing on any predefined feature, in order to reproduce all its computational characteristics at once. In this work, we propose two new deep generative models of realistic SAT instances, and carry out an exhaustive experimental evaluation of these and other existing models in order to analyze their performances. Our results show that models based on graph convolutional networks, possibly enhanced with edge features, return the best results in terms of structural properties and SAT solver performance.

BibTeX - Entry

@InProceedings{garzon_et_al:LIPIcs.SAT.2022.3,
  author =	{Garz\'{o}n, Iv\'{a}n and Mesejo, Pablo and Gir\'{a}ldez-Cru, Jes\'{u}s},
  title =	{{On the Performance of Deep Generative Models of Realistic SAT Instances}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{3:1--3:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16677},
  URN =		{urn:nbn:de:0030-drops-166775},
  doi =		{10.4230/LIPIcs.SAT.2022.3},
  annote =	{Keywords: Realistic SAT generators, pseudo-industrial random SAT, deep generative models, deep learning}
}

Keywords: Realistic SAT generators, pseudo-industrial random SAT, deep generative models, deep learning
Collection: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue Date: 2022
Date of publication: 28.07.2022

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