Towards better heuristics for solving bounded model checking problems

Ábrahám, E., Schubert, T., Becker, B., Fränzle, M., & Herde, C. (2007). Parallel sat solving in bounded model checking. In L. Brim, B. Haverkort, M. Leucker, & J. van de Pol (Eds.) Formal Methods: Applications and Technology (pp. 301–315). Berlin: Springer. Aloul, F.A., Sakallah, K.A., & Markov, I.L. (2006). Efficient symmetry breaking for boolean satisfiability. IEEE Transactions on Computers, 55 (5), 549–558. https://doi.org/10.1109/TC.2006.75. Ansótegui, C., Giráldez-Cru, J., & Levy, J. (2012). The community structure of sat formulas. In A. Cimatti R. Sebastiani (Eds.) Theory and Applications of Satisfiability Testing – SAT (pp. 410–423). Springer. Ansótegui, C., Bonet, M.L., Giráldez-Cru, J., Levy, J., & Simon, L. (2019). Community structure in industrial sat instances. arXiv:1606.03329. Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.M., & Piette, C. (2012). Revisiting clause exchange in parallel sat solving. In 15th International Conference on Theory and Applications of Satisfiability Testing (SAT’12), of Lecture notes in computer science (LNCS). Available from: https://hal.archives-ouvertes.fr/hal-00865596, (Vol. 7962 pp. 200–213). Trento: Springer. Baier, C., & Katoen, J.P. (2008). Principles of Model Checking. Cambridge: The MIT Press. Balyo, T., Sanders, P., & Sinz, C. (2015). Hordesat: A massively parallel portfolio sat solver. arXiv:1505.03340. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., & Zhu, Y. (2003). Bounded model checking, vol. 12. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., & Hwang, L.J. (1992). Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2), 142–170. https://doi.org/10.1016/0890-5401(92)90017-A. Cheng, X., Zhou, M., Song, X., Gu, M., & Sun, J. (2018). Parallelizing smt solving: Lazy decomposition and conciliation. Artificial Intelligence, 257, 127–157. Available from: https://www.sciencedirect.com/science/article/pii/S0004370218300237. https://doi.org/10.1016/j.artint.2018.01.001. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., & Tacchella, A. (2002). NuSMV Version 2: an opensource tool for symbolic model checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), of LNCS, Vol. 2404. Copenhagen: Springer. Clarke, E., McMillan, K., Campos, S., & Hartonas-Garmhausen, V. (1996). Symbolic model checking. In R. Alur T. A. Henzinger (Eds.) Computer Aided Verification (pp. 419–422). Berlin: Springer. Clarke, E., Biere, A., Raimi, R., & Zhu, Y. (2001). Bounded model checking using satisfiability solving. Form. Methods Syst. Des., 19(1), 7–34. Availablefrom: https://doi.org/10.1023/A:1011276507260. Clarke, E., Emerson, E., & Sifakis, J. (2009). Model checking. Communications of the ACM, 52(11). https://doi.org/10.1145/1592761.1592781. Clarke, E.M., Klieber, W., Nováček, M., & Zuliani, P. (2012). Model Checking and the State Explosion Problem, (pp. 1–30). Berlin: Springer. Crawford, J., Ginsberg, M., Luks, E., & Roy, A. (1996). Symmetry-breaking predicates for search problems. In Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, KR’96 (pp. 148–159). San Francisco: Morgan Kaufmann Publishers Inc. Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Available from: https://doi.org/10.1145/368273.368557, (Vol. 5 pp. 394–397). Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., & Xu, L. (2016). Spot 2.0 — a framework for LTL and ω-automata manipulation. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16), of lecture notes in computer science, (Vol. 9938 pp. 122–129). Springer. Eén, N., & Soörensson, N. (2004). An extensible sat-solver. In E. Giunchiglia A. Tacchella (Eds.) Theory and Applications of Satisfiability Testing (pp. 502–518). Berlin: Springer. Frost, D., & Dechter, R. (2000). Dead-end driven learning. Proceedings of the National Conference on Artificial Intelligence, 1(08). Ganai, M., & Gupta, A. (2008). Tunneling and slicing: Towards scalable bmc. In Proceedings of the 45th Annual Design Automation Conference, DAC ’08 (pp. 137–142). New York: Association for Computing Machinery. Available from: https://doi.org/10.1145/1391469.1391507. Ganai, M., Gupta, A., Yang, Z., & Ashar, P. (2006). Efficient distributed sat and sat-based distributed bounded model checking. International Journal on Software Tools for Technology Transfer, 8, 387–396. https://doi.org/10.1007/s10009-005-0203-z. Ganai, M. K. (2007). Sat-based scalable formal verification solutions. In In Series on Integrated Circuits and Systems. New York: Springer. Ganai, M.K. (2010). Propelling SAT and sat-based BMC using careset. In R. Bloem N. Sharygina (Eds.) Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD (pp. 231–238). Lugano: IEEE. Available from: http://ieeexplore.ieee.org/document/5770954/. Ginsberg, M.L., & McAllester, D.A. (1994). In A. Borning (Ed.) PPCP. Lecture Notes in Computer Science. Available from: http://dblp.uni-trier.de/db/conf/ppcp/ppcp94-lncs.html#GinsbergM94, (Vol. 874 pp. 243–265). Springer. Guo, L., Hamadi, Y., Jabbour, S., & Sais, L. (2010). Diversification and intensification in parallel sat solving. In D. Cohen (Ed.) Principles and Practice of Constraint Programming - CP 2010 (pp. 252–265). Berlin: Springer. Guo, L., Hamadi, Y., Jabbour, S., & Saïs, L. (2010). Diversification and intensification in parallel SAT Solving. In 16th International Conference on Principles and Practice of Constraint Programming (CP’10). United Kingdom (pp. 252–265). Available from: https://hal.archives-ouvertes.fr/hal-00865417. Hamadi, Y., Jabbour, S., & Sais, L. (2009). Manysat: a parallel sat solver. Journal on Satisfiability, Boolean Modeling and Computation, 6 (4), 245–262. Available from: http://dblp.uni-trier.de/db/journals/jsat/jsat6.html#HamadiJS09. Hamadi, Y., Marques-Silva, J., & Wintersteiger, C.M. (2011). Lazy decomposition for distributed decision procedures. In Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC’11), (Vol. 72 pp. 43–54). Holzmann, G.J. (2018). Explicit-state model checking. In E.M. Clarke, T.A. Henzinger, H. Veith, & R. Bloem (Eds.) Handbook of Model Checking (pp. 153–171). Cham: Springer International Publishing. Available from: https://doi.org/10.1007/978-3-319-10575-8_5. Jabbour, S., Lazaar, N., Hamadi, Y., & Sebag, M. (2012). Cooperation control in parallel SAT solving: a multi-armed bandit approach. In Workshop on Bayesian Optimization and Decision Making. Lake Tahoe, United States. Available from: https://hal.archives-ouvertes.fr/hal-00870946. Jackson, P., & Sheridan, D. (2005). Clause form conversions for boolean circuits. In H.H. Hoos D.J. Mitchell (Eds.) Theory and Applications of Satisfiability Testing (pp. 183–198). Berlin: Springer. Jamali, S., & Mitchell, D. (2018). Centrality-based improvements to cdcl heuristics. In O. Beyersdorff C. M. Wintersteiger (Eds.) Theory and Applications of Satisfiability Testing - SAT 2018 (pp. 122–131). Cham: Springer International Publishing. Katsirelos, G., & Simon, L. (2012). Eigenvector centrality in industrial sat instances. In M. Milano (Ed.) Principles and Practice of Constraint Programming (pp. 348–356). Berlin: Springer. Kaufmann, M., & Kottler, S. (2011). Sartagnan - a parallel portfolio sat solver with lockless physical clause sharing. In In Pragmatics of SAT. Kheireddine, A., Renault, E., & Baarir, S. (2021). Towards better heuristics for solving bounded model checking problems. In L.D. Michel (Ed.) 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Available from: https://drops.dagstuhl.de/opus/volltexte/2021/15298, (Vol. 210 pp. 7:1–7:11). Dagstuhl: Leibniz International Proceedings in Informatics (LIPIcs). Le Frioux, L., Baarir, S., Sopena, J., & Kordon, F. (2017). PainleSS: a framework for parallel SAT solving. In Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT’17), Lecture Notes in Computer Science, (Vol. 10491 pp. 233–250). Cham: Springer. Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K., & Poupart, P. (2016). Learning rate based branching heuristic for sat solvers. In SAT. Manna, Z., & Pnueli, A. (1990). A hierarchy of temporal properties (invited paper, 1989). In PODC ’90. Metin, H., Baarir, S., Colange, M., & Kordon, F. (2018). 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), Lecture Notes in Computer Science, (Vol. 10805 pp. 99–114). Thessaloniki: Springer. Pelánek, R. (2007). Beem: Benchmarks for explicit model checkers. In D. Bošnački S. Edelkamp (Eds.) Model Checking Software (pp. 263–267). Berlin: Springer. Rozier, K.Y. (2011). Survey: Linear temporal logic symbolic model checking. Computer Science Review, 5(2), 163–203. Available from: https://doi.org/10.1016/j.cosrev.2010.06.002. Cherif, M.S., Habet, D., & Terrioux, C. (2021). Un bandit manchot pour combiner CHB et VSIDS. In Actes des 16èmes Journées Francophones de Programmation par Contraintes (JFPC), Nice, France. Available from: https://hal-amu.archives-ouvertes.fr/hal-03270931. Schaefer, T.J. (1978). The complexity of satisfiability problems. In Proceedings of the Tenth Annual ACM Symposium on Theory of Computing, STOC ’78 (pp. 216–226). New York: Association for Computing Machinery. Available from: https://doi.org/10.1145/800133.804350. Shtrichman, O. (2000). Tuning sat checkers for bounded model checking. In E. A. Emerson A. P. Sistla (Eds.) Computer Aided Verification (pp. 480–494). Berlin: Springer. Marques Silva, J.P., & Sakallah, K.A. (1997). Grasp—a new search algorithm for satisfiability. In Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD ’96 (pp. 220–227). USA: IEEE Computer Society. Simon, L., & Audemard, G. (2009). Predicting learnt clauses quality in modern SAT solver. In Twenty-first International Joint Conference on Artificial Intelligence (IJCAI’09), Pasadena, United States. Available from: https://hal.inria.fr/inria-00433805. Wang, C., Jin, H., Hachtel, G.D., & Somenzi, F. (2004). Refining the sat decision ordering for bounded model checking. In Proceedings of the 41st Annual Design Automation Conference, DAC ’04 (pp. 535–538). New York: Association for Computing Machinery. Available from: https://doi.org/10.1145/996566.996713. Wieringa, S. (2011). On incremental satisfiability and bounded model checking. CEUR Workshop Proceedings, 832, 13–21. Zarpas, E. (2004). Simple yet efficient improvements of sat based bounded model checking. In A. J. Hu E. K. Martin (Eds.) Formal Methods in Computer-Aided Design (pp. 174–185). Berlin: Springer. Zhang, H., Bonacina, M.P., & Hsiang, J. (1996). Psato: a distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation, 21, 543–560. https://doi.org/10.1006/jsco.1996.0030. Zhang, L., Madigan, C.F., Moskewicz, M.W., & Malik, S. (2001). Efficient conflict driven learning in a boolean satisfiability solver. In Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD ’01 (pp. 279–285). IEEE Press.