2026-09-22T20:11:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18465 2026-09-05T15:01:46Z ddc:004 open_access

CadiBack: Extracting Backbones with CaDiCaL Biere, Armin Froleyks, Nils Wang, Wenxi Satisfiability Backbone Incremental Solving 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Armin Biere and Nils Froleyks and Wenxi Wang 2023 Is Part Of LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2023.3 urn:nbn:de:0030-drops-184655 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.3 eng https://creativecommons.org/licenses/by/4.0/legalcode