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.ITP.2021.9
URN: urn:nbn:de:0030-drops-139043
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13904/
Go to the corresponding LIPIcs Volume Portal


Besson, Frédéric

Itauto: An Extensible Intuitionistic SAT Solver

pdf-format:
LIPIcs-ITP-2021-9.pdf (0.8 MB)


Abstract

We present the design and implementation of itauto, a Coq reflexive tactic for intuitionistic propositional logic. The tactic inherits features found in modern SAT solvers: definitional conjunctive normal form; lazy unit propagation and conflict driven backjumping. Formulae are hash-consed using native integers thus enabling a fast equality test and a pervasive use of Patricia Trees. We also propose a hybrid proof by reflection scheme whereby the extracted solver calls user-defined tactics on the leaves of the propositional proof search thus enabling theory reasoning and the generation of conflict clauses. The solver has decent efficiency and is more scalable than existing tactics on synthetic benchmarks and preliminary experiments are encouraging for existing developments.

BibTeX - Entry

@InProceedings{besson:LIPIcs.ITP.2021.9,
  author =	{Besson, Fr\'{e}d\'{e}ric},
  title =	{{Itauto: An Extensible Intuitionistic SAT Solver}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13904},
  URN =		{urn:nbn:de:0030-drops-139043},
  doi =		{10.4230/LIPIcs.ITP.2021.9},
  annote =	{Keywords: SAT solver, proof by reflection}
}

Keywords: SAT solver, proof by reflection
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Software: https://gitlab.inria.fr/fbesson/itauto archived at: https://archive.softwareheritage.org/swh:1:dir:986dc28c9844ba2faedc3d134b2acfb31e8c27c4


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