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.2023.21
URN: urn:nbn:de:0030-drops-184837
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18483/
Go to the corresponding LIPIcs Volume Portal

Pollitt, Florian ; Fleury, Mathias ; Biere, Armin

Faster LRAT Checking Than Solving with CaDiCaL

pdf-format:
LIPIcs-SAT-2023-21.pdf (0.8 MB)

Abstract

DRAT is the standard proof format used in the SAT Competition. It is easy to generate but checking proofs often takes even more time than solving the problem. An alternative is to use the LRAT proof system. While LRAT is easier and way more efficient to check, it is more complex to generate directly. Due to this complexity LRAT is not supported natively by any state-of-the-art SAT solver. Therefore Carneiro and Heule proposed the mixed proof format FRAT which still suffers from costly intermediate translation. We present an extension to the state-of-the-art solver CaDiCaL which is able to generate LRAT natively for all procedures implemented in CaDiCaL. We further present Lrat-Trim, a tool which not only trims and checks LRAT proofs in both ASCII and binary format but also produces clausal cores and has been tested thoroughly. Our experiments on recent competition benchmarks show that our approach reduces time of proof generation and certification substantially compared to competing approaches using intermediate DRAT or FRAT proofs.

BibTeX - Entry

@InProceedings{pollitt_et_al:LIPIcs.SAT.2023.21,
  author =	{Pollitt, Florian and Fleury, Mathias and Biere, Armin},
  title =	{{Faster LRAT Checking Than Solving with CaDiCaL}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{21:1--21:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18483},
  URN =		{urn:nbn:de:0030-drops-184837},
  doi =		{10.4230/LIPIcs.SAT.2023.21},
  annote =	{Keywords: SAT solving, Proof Checking, DRAT, LRAT, FRAT}
}

Keywords: SAT solving, Proof Checking, DRAT, LRAT, FRAT
Collection: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Issue Date: 2023
Date of publication: 09.08.2023
Supplementary Material: Dataset (Log files): https://cca.informatik.uni-freiburg.de/lrat/

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