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.3
URN: urn:nbn:de:0030-drops-184655
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18465/
Biere, Armin ;
Froleyks, Nils ;
Wang, Wenxi
CadiBack: Extracting Backbones with CaDiCaL
Abstract
The backbone of a satisfiable formula is the set of literals that are true in all its satisfying assignments. Backbone computation can improve a wide range of SAT-based applications, such as verification, fault localization and product configuration. In this tool paper, we introduce a new backbone extraction tool called CadiBack. It takes advantage of unique features available in our state-of-the-art SAT solver CaDiCaL including transparent inprocessing and single clause assumptions, which have not been evaluated in this context before. In addition, CaDiCaL is enhanced with an improved algorithm to support model rotation by utilizing watched literal data structures. In our comprehensive experiments with a large number of benchmarks, CadiBack solves 60% more instances than the state-of-the-art backbone extraction tool MiniBones. Our tool is thoroughly tested with fuzzing, internal correctness checking and cross-checking on a large benchmark set. It is publicly available as open source, well documented and easy to extend.
BibTeX - Entry
@InProceedings{biere_et_al:LIPIcs.SAT.2023.3,
author = {Biere, Armin and Froleyks, Nils and Wang, Wenxi},
title = {{CadiBack: Extracting Backbones with CaDiCaL}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {3:1--3: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/18465},
URN = {urn:nbn:de:0030-drops-184655},
doi = {10.4230/LIPIcs.SAT.2023.3},
annote = {Keywords: Satisfiability, Backbone, Incremental Solving}
}
