DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2022.3

On the Performance of Deep Generative Models of Realistic SAT Instances

Authors: Iván Garzón, Pablo Mesejo, and Jesús Giráldez-Cru

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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.

Cite as

Iván Garzón, Pablo Mesejo, and Jesús Giráldez-Cru. On the Performance of Deep Generative Models of Realistic SAT Instances. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.SAT.2022.3},
  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}
}

Search Results

Documents authored by Garzón, Iván

On the Performance of Deep Generative Models of Realistic SAT Instances

Abstract

Cite as

Thanks for your feedback!

Could not send message