Tags:Backbone Extraction, Clause Assumption, Incremental Solving, Inprocessing and Model Rotation
Abstract:
The backbone of a satisfiable formula is the set of literals that are always true in all its satisfying assignments. Computing the backbone efficiently is able to 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 using single clause assumption, 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 publicly available as open source, well documented and easy to extend as well as thoroughly tested through fuzzing, internal correctness checking and cross checking on a large benchmark set.