Armin Biere, Nils Froleyks, Wenxi Wang,
"CadiBack: Extracting Backbones with CaDiCaL"
, in Mahajan, Meena und Slivovsky, Friedrich: 26th International Conference on Theory andApplications of Satisfiability Testing, SAT 2023, Serie LIPIcs, Vol. 271, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Seite(n) 3:1-3:12, 8-2023
Original Titel:
CadiBack: Extracting Backbones with CaDiCaL
Sprache des Titels:
Englisch
Original Buchtitel:
26th International Conference on Theory andApplications of Satisfiability Testing, SAT 2023
Original Kurzfassung:
The backbone of a satisfiable formula is the set ofliterals that are true in all its satisfying assignments. Backbonecomputation can improve a wide range of SAT-based applications, suchas verification, fault localization and product configuration. Inthis tool paper, we introduce a new backbone extraction tool calledCadiBack. It takes advantage of unique features available in ourstate-of- the-art SAT solver CaDiCaL including transparentinprocessing and single clause assumptions, which have not beenevaluated in this context before. In addition, CaDiCaL is enhancedwith an improved algorithm to support model rotation by utilizingwatched literal data structures. In our comprehensive experimentswith a large number of benchmarks, CadiBack solves 60\% moreinstances than the state-of-the-art backbone extraction toolMiniBones. Our tool is thoroughly tested with fuzzing, internalcorrectness checking and cross-checking on a large benchmark set. Itis publicly available as open source, well documented and easy toextend.
Forschungs-