Document Open Access Logo

Towards Better Heuristics for Solving Bounded Model Checking Problems (Short Paper)

Authors Anissa Kheireddine , Etienne Renault , Souheib Baarir

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.7.pdf
  • Filesize: 0.75 MB
  • 11 pages

Document Identifiers

Author Details

Anissa Kheireddine
  • EPITA, LRDE, Kremlin-Bicêtre, France
  • Sorbonne Université, UMR 7606 LIP6, Paris, France
Etienne Renault
  • EPITA, LRDE, Kremlin-Bicêtre, France
Souheib Baarir
  • Sorbonne Université, CNRS UMR 7606 LIP6, France
  • Université Paris Nanterre, France

Cite As Get BibTex

Anissa Kheireddine, Etienne Renault, and Souheib Baarir. Towards Better Heuristics for Solving Bounded Model Checking Problems (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 7:1-7:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CP.2021.7

Abstract

This paper presents a new way to improve the performance of the SAT-based bounded model checking problem by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approach with two new heuristics: Structure-based and Linear Programming heuristics and show promising results.

Subject Classification

ACM Subject Classification
  • Hardware → Theorem proving and SAT solving
  • Hardware → Model checking
Keywords
  • Bounded model checking
  • SAT
  • Structural information
  • Linear Programming

Metrics

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

Supplementary Materials

References

  1. F.A. Aloul, K.A. Sakallah, and I.L. Markov. Efficient symmetry breaking for boolean satisfiability. IEEE Transactions on Computers, 55(5):549-558, 2006. URL: https://doi.org/10.1109/TC.2006.75.
  2. Carlos Ansótegui, Jesús Giráldez-Cru, and Jordi Levy. The community structure of sat formulas. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012, pages 410-423, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  3. Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, Jordi Levy, and Laurent Simon. Community structure in industrial sat instances, 2019. URL: http://arxiv.org/abs/1606.03329.
  4. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  5. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. Bounded model checking, December 2003. URL: https://doi.org/10.1016/S0065-2458(03)58003-2.
  6. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142-170, 1992. URL: https://doi.org/10.1016/0890-5401(92)90017-A.
  7. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), volume 2404 of LNCS, Copenhagen, Denmark, July 2002. Springer. Google Scholar
  8. E. Clarke, K. McMillan, S. Campos, and V. Hartonas-Garmhausen. Symbolic model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification, pages 419-422, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. Google Scholar
  9. Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Form. Methods Syst. Des., 19(1):7–34, 2001. URL: https://doi.org/10.1023/A:1011276507260.
  10. Edmund Clarke, E. Emerson, and Joseph Sifakis. Model checking. Communications of the ACM, 52, November 2009. URL: https://doi.org/10.1145/1592761.1592781.
  11. James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy. Symmetry-breaking predicates for search problems. In Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, KR'96, page 148–159, San Francisco, CA, USA, 1996. Morgan Kaufmann Publishers Inc. Google Scholar
  12. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394–397, July 1962. URL: https://doi.org/10.1145/368273.368557.
  13. Daniel Frost and Rina Dechter. Dead-end driven learning. Proceedings of the National Conference on Artificial Intelligence, 1, August 2000. Google Scholar
  14. Malay Ganai and Aarti Gupta. Tunneling and slicing: Towards scalable bmc. In Proceedings of the 45th Annual Design Automation Conference, DAC '08, page 137–142, New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1391469.1391507.
  15. Malay Ganai, Aarti Gupta, Zijiang Yang, and Pranav Ashar. Efficient distributed sat and sat-based distributed bounded model checking. International Journal on Software Tools for Technology Transfer, 8:387-396, August 2006. URL: https://doi.org/10.1007/s10009-005-0203-z.
  16. Malay K. Ganai. Sat-based scalable formal verification solutions. In Series on Integrated Circuits and Systems, Springer-Verlag New York, 2007. Google Scholar
  17. Malay K. Ganai. Propelling SAT and sat-based BMC using careset. In Roderick Bloem and Natasha Sharygina, editors, Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pages 231-238. IEEE, 2010. URL: http://ieeexplore.ieee.org/document/5770954/.
  18. Matthew L. Ginsberg and David A. McAllester. Gsat and dynamic backtracking. In Alan Borning, editor, PPCP, volume 874 of Lecture Notes in Computer Science, pages 243-265. Springer, 1994. URL: http://dblp.uni-trier.de/db/conf/ppcp/ppcp94-lncs.html#GinsbergM94.
  19. Gerard J. Holzmann. Explicit-state model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 153-171, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-10575-8_5.
  20. Paul Jackson and Daniel Sheridan. Clause form conversions for boolean circuits. In Holger H. Hoos and David G. Mitchell, editors, Theory and Applications of Satisfiability Testing, pages 183-198, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  21. Sima Jamali and David Mitchell. Centrality-based improvements to cdcl heuristics. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018, pages 122-131, Cham, 2018. Springer International Publishing. Google Scholar
  22. George Katsirelos and Laurent Simon. Eigenvector centrality in industrial sat instances. In Michela Milano, editor, Principles and Practice of Constraint Programming, pages 348-356, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  23. J. Liang, Vijay Ganesh, P. Poupart, and K. Czarnecki. Learning rate based branching heuristic for sat solvers. In SAT, 2016. Google Scholar
  24. Z. Manna and A. Pnueli. A hierarchy of temporal properties (invited paper, 1989). In PODC '90, 1990. Google Scholar
  25. Hakan Metin, Souheib Baarir, Maximilien Colange, and Fabrice Kordon. Cdclsym: Introducing effective symmetry breaking in sat solving. In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), volume 10805 of Lecture Notes in Computer Science, pages 99-114, Thessaloniki, Greece, 2018. Springer. Google Scholar
  26. Radek Pelánek. Beem: Benchmarks for explicit model checkers. In Dragan Bošnački and Stefan Edelkamp, editors, Model Checking Software, pages 263-267, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  27. Kristin Y. Rozier. Survey: Linear temporal logic symbolic model checking. Comput. Sci. Rev., 5(2):163–203, 2011. URL: https://doi.org/10.1016/j.cosrev.2010.06.002.
  28. Thomas J. Schaefer. The complexity of satisfiability problems. In Proceedings of the Tenth Annual ACM Symposium on Theory of Computing, STOC '78, page 216–226, New York, NY, USA, 1978. Association for Computing Machinery. URL: https://doi.org/10.1145/800133.804350.
  29. Ofer Shtrichman. Tuning sat checkers for bounded model checking. In E. Allen Emerson and Aravinda Prasad Sistla, editors, Computer Aided Verification, pages 480-494, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. Google Scholar
  30. João P. Marques Silva and Karem A. Sakallah. Grasp—a new search algorithm for satisfiability. In Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD '96, page 220–227, USA, 1997. IEEE Computer Society. Google Scholar
  31. Laurent Simon and Gilles Audemard. Predicting Learnt Clauses Quality in Modern SAT Solver. In Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), Pasadena, United States, 2009. URL: https://hal.inria.fr/inria-00433805.
  32. Chao Wang, HoonSang Jin, Gary D. Hachtel, and Fabio Somenzi. Refining the sat decision ordering for bounded model checking. In Proceedings of the 41st Annual Design Automation Conference, DAC '04, page 535–538, New York, NY, USA, 2004. Association for Computing Machinery. URL: https://doi.org/10.1145/996566.996713.
  33. Emmanuel Zarpas. Simple yet efficient improvements of sat based bounded model checking. In Alan J. Hu and Andrew K. Martin, editors, Formal Methods in Computer-Aided Design, pages 174-185, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  34. Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, and Sharad Malik. Efficient conflict driven learning in a boolean satisfiability solver. In Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD '01, page 279–285. IEEE Press, 2001. 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 About DROPS Imprint Privacy Contact