Document Open Access Logo

CadiBack: Extracting Backbones with CaDiCaL

Authors Armin Biere , Nils Froleyks , Wenxi Wang

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.3.pdf
  • Filesize: 0.99 MB
  • 12 pages

Document Identifiers

Author Details

Armin Biere
  • Universität Freiburg, Germany
Nils Froleyks
  • Johannes Kepler Universität, Linz, Austria
Wenxi Wang
  • University of Texas at Austin, TX, USA

Cite AsGet BibTex

Armin Biere, Nils Froleyks, and Wenxi Wang. CadiBack: Extracting Backbones with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.3

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Satisfiability
  • Backbone
  • Incremental Solving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Anton Belov and João Marques-Silva. Accelerating MUS extraction with recursive model rotation. In Per Bjesse and Anna Slobodová, editors, International Conference on Formal Methods in Computer-Aided Design, FMCAD '11, Austin, TX, USA, October 30 - November 02, 2011, pages 37-40. FMCAD Inc., 2011. Google Scholar
  2. Armin Biere. Adaptive restart strategies for conflict driven SAT solvers. In Hans Kleine Büning and Xishun Zhao, editors, Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, volume 4996 of Lecture Notes in Computer Science, pages 28-33. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79719-7_4.
  3. Armin Biere and Mathias Fleury. Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022. In Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions, volume B-2022-1 of Department of Computer Science Series of Publications B, pages 10-11. University of Helsinki, 2022. Google Scholar
  4. Armin Biere, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba entering the SAT Competition 2021. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2021 - Solver and Benchmark Descriptions, volume B-2021-1 of Department of Computer Science Report Series B, pages 10-13. University of Helsinki, 2021. Google Scholar
  5. Armin Biere and Andreas Fröhlich. Evaluating CDCL variable scoring schemes. In Marijn Heule and Sean A. Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, volume 9340 of Lecture Notes in Computer Science, pages 405-422. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_29.
  6. Armin Biere, Nils Froleyks, and Wenxi Wang. Sampled and Normalized Satisfiable Instances from the main track of the SAT Competition 2004 to 2022, March 2023. URL: https://doi.org/10.5281/zenodo.7750076.
  7. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 391-435. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200992.
  8. Armin Biere, Matti Järvisalo, Daniel Le Berre, Kuldeep S. Meel, and Stefan Mengel. The SAT practitioner’s manifesto, September 2020. URL: https://doi.org/10.5281/zenodo.4500928.
  9. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_6.
  10. Sharlee Climer and Weixiong Zhang. Searching for backbones and fat: A limit-crossing approach with applications. In AAAI/IAAI, pages 707-712, 2002. Google Scholar
  11. Michael Codish, Yoav Fekete, and Amit Metodi. Backbones for equality. In Valeria Bertacco and Axel Legay, editors, Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings, volume 8244 of Lecture Notes in Computer Science, pages 1-14. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03077-7_1.
  12. Olivier Dubois and Gilles Dequen. A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In IJCAI, volume 1, pages 248-253, 2001. Google Scholar
  13. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  14. Mohamed El Bachir Menaï. A two-phase backbone-based search heuristic for partial MAX-SAT-an initial investigation. In Innovations in Applied Artificial Intelligence: 18th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, IEA/AIE 2005, Bari, Italy, June 22-24, 2005. Proceedings 18, pages 681-684. Springer, 2005. Google Scholar
  15. Katalin Fazekas, Armin Biere, and Christoph Scholl. Incremental inprocessing in SAT solving. In Mikoláš Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 136-154. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_9.
  16. Nils Froleyks and Armin Biere. Single clause assumption without activation literals to speed-up IC3. In Formal Methods in Computer Aided Design, FMCAD 2021, pages 72-76. IEEE, 2021. URL: https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_15.
  17. Mikoláš Janota. SAT solving in interactive configuration. PhD thesis, University College Dublin, 2010. Google Scholar
  18. Mikoláš Janota, Inês Lynce, and João Marques-Silva. Algorithms for computing backbones of propositional formulae. AI Commun., 28(2):161-177, 2015. URL: https://doi.org/10.3233/AIC-140640.
  19. Andreas Kaiser and Wolfgang Küchlin. Detecting inadmissible and necessary variables in large propositional formulae. In Intl. Joint Conf. on Automated Reasoning (Short Papers), pages 96-102. University of Siena, 2001. Google Scholar
  20. Philip Kilby, John Slaney, Sylvie Thiébaux, Toby Walsh, et al. Backbones and backdoors in satisfiability. In AAAI, volume 5, pages 1368-1373, 2005. Google Scholar
  21. D. Richard Kuhn, Dolores R. Wallace, and Albert M. Gallo. Software fault interactions and implications for software testing. IEEE Trans. Software Eng., 30(6):418-421, 2004. URL: https://doi.org/10.1109/TSE.2004.24.
  22. João Marques-Silva, Mikoláš Janota, and Inês Lynce. On computing backbones of propositional theories. In Helder Coelho, Rudi Studer, and Michael J. Wooldridge, editors, ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 15-20. IOS Press, 2010. Google Scholar
  23. Rémi Monasson, Riccardo Zecchina, Scott Kirkpatrick, Bart Selman, and Lidror Troyansky. Determining computational complexity from characteristic ‘phase transitions’. Nature, 400(6740):133-137, 1999. Google Scholar
  24. Andrew J. Parkes. Clustering at the phase transition. In Benjamin Kuipers and Bonnie L. Webber, editors, Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31, 1997, Providence, Rhode Island, USA, pages 340-345. AAAI Press / The MIT Press, 1997. Google Scholar
  25. Alessandro Previti and Matti Järvisalo. A preference-based approach to backbone computation with application to argumentation. In Proceedings of the 33rd Annual ACM Symposium on Applied Computing, pages 896-902, 2018. Google Scholar
  26. Miroslav N Velev. Formal verification of vliw microprocessors with speculative execution. In Computer Aided Verification: 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings 12, pages 296-311. Springer, 2000. Google Scholar
  27. Ryan Williams, Carla P. Gomes, and Bart Selman. Backdoors to typical case complexity. In Georg Gottlob and Toby Walsh, editors, IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003, pages 1173-1178. Morgan Kaufmann, 2003. Google Scholar
  28. Guoqiang Zeng, Chongwei Zheng, Zhengjiang Zhang, and Yongzai Lu. An backbone guided extremal optimization method for solving the hard maximum satisfiability problem. In 2012 International Conference on Computer Application and System Modeling, pages 1301-1304. Atlantis Press, 2012. Google Scholar
  29. Weixiong Zhang. Configuration landscape analysis and backbone guided local search.: Part i: Satisfiability and maximum satisfiability. Artificial Intelligence, 158(1):1-26, 2004. Google Scholar
  30. Weixiong Zhang. Phase transitions and backbones of the asymmetric traveling salesman problem. Journal of Artificial Intelligence Research, 21:471-497, 2004. Google Scholar
  31. Weixiong Zhang, Ananda Rangan, Moshe Looks, et al. Backbone guided local search for maximum satisfiability. In IJCAI, volume 3, pages 1179-1186, 2003. Google Scholar
  32. Yueling Zhang, Min Zhang, and Geguang Pu. Optimizing backbone filtering. Science of Computer Programming, 187:102374, 2020. Google Scholar
  33. Yueling Zhang, Min Zhang, Geguang Pu, Fu Song, and Jianwen Li. Towards backbone computing: A greedy-whitening based approach. AI Communications, 31(3):267-280, 2018. Google Scholar
  34. Charlie Shucheng Zhu, Georg Weissenbacher, and Sharad Malik. Post-silicon fault localisation using maximum satisfiability and backbones. In 2011 Formal Methods in Computer-Aided Design (FMCAD), pages 63-66. IEEE, 2011. Google Scholar
  35. Charlie Shucheng Zhu, Georg Weissenbacher, and Sharad Malik. Silicon fault diagnosis using sequence interpolation with backbones. In Yao-Wen Chang, editor, The IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2014, San Jose, CA, USA, November 3-6, 2014, pages 348-355. IEEE, 2014. URL: https://doi.org/10.1109/ICCAD.2014.7001373.
  36. Charlie Shucheng Zhu, Georg Weissenbacher, Divjyot Sethi, and Sharad Malik. SAT-based techniques for determining backbones for post-silicon fault localisation. In 2011 IEEE International High Level Design Validation and Test Workshop, pages 84-91. IEEE, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact