Abstract
With the growing scale and complexity of software and hardware designs, model checking generally results in the combination explosion of state space. Predicate abstraction is an important technique to solve this problem. The number of refinement iterations will be reduced by extracting the unsatisfiable cores. The smaller unsatisfiable cores are, the more false counterexamples are eliminated. Therefore, a fast algorithm of deriving the minimum unsatisfiable cores is employed in the formal verification tool of hardware. The two optimal algorithms of computing minimum unsatisfiable cores are compared on the instruction Cache unit of a microprocessor. The experimental results showed that the greedy-generic algorithm outperforms the branch-bound algorithm. Furthermore we analyzed that the unsatisfiable cores plays an important role in predicate abstraction, and it can improve the efficiency of model checking.
Supported by the National Natural Science Foundation of China under grant No. 62072464 and U19A2062, and the National Laboratory of Parallel and Distributed Processing Open Fund under grant No. WDZC20205500116.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Moskewicz, M.W., Madigan, C.F., Zhao Y., et al.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, pp. 530–535. ACM, Las Vegas, USA (2001)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37
Jain, H., Kroening, D.: Word level predicate abstraction and refinement for verifying RTL Verilog. In: Proceedings of the 42nd Design Automation Conference, pp. 445–450. ACM, Anaheim, San Diego, USA (2005)
Liffiton, M.H., Mneimneh, M.N., Lynce, I., et al.: A branch and bound algorithm for extracting smallest minimal unsatisfiable formulas. Constraints 14(4), 415–442 (2009)
Zhang, J.M., Li, S.K., Shen, S.Y.: Algorithms for Deriving minimum unsatisfiable Boolean subformulae. Acta Electronica Sinica 37(3), 56–59 (2009)
Lynce, I., Marques-silva, J.: On computing minimum unsatisfiable cores, In: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, pp. 305–310. Springer, Vancouver (2004)
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40, 1–30 (2008)
Gershman, R., Koifman, M., Strichman, O.: An approach for extracting a small unsatisfiable core. Formal Method Syst. Des. 33(1), 1–27 (2008)
Gregoire, E., Mazuer, B., Piette, C.: Using local search to find MSSes and MUSes. Eur. J. Oper. Res. 199(3), 640–646 (2009)
Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Proceedings of 10th International Conference Formal Methods in Computer Aided Design, pp. 221–229. IEEE, Lugano, Switzerland (2010)
Ryvchin, V., Strichman, O.: Faster extraction of high-level minimal unsatisfiable cores. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 174–187. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_15
Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. J. AI Commun. 25(2), 97–116 (2012)
Nadel, A., Ryvchin, V., Strichman, O.: Efficient MUS extraction with resolution. In: Proceedings 13th International Conference Formal Methods in Computer Aided Design, pp. 197–200. IEEE, Portland, OR, USA (2013)
Belov, A., Heule, M.J.H., Marques-Silva, J.: MUS extraction using clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 48–57. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_5
Bacchus, F., Katsirelos, G.: Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 70–86. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_5
Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 35–44. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33954-2_3
Zhao, W., Liffiton, M.H.: Parallelizing partial MUS enumeration. In: Proceedings of IEEE 28th International Conference on Tools with Artificial Intelligence, pp. 464–471. IEEE, San Jose, CA, USA (2016)
Gregoire, E., Izza Y.: Boosting MCSes enumeration. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence, pp. 1309–1315. ACM, Stockholm, Sweden (2018)
Narodytska, N., Bjorner, N., Marinescu, M.C., et al.: Core-guided minimal correction set and core enumeration. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence, pp. 1353–1361. ACM, Stockholm, Sweden (2018)
Liu, S., Luo, J.: FMUS2: an efficient algorithm to compute minimal unsatisfiable subsets. In: Fleuriot, J., Wang, D., Calmet, J. (eds.) AISC 2018. LNCS (LNAI), vol. 11110, pp. 104–118. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99957-9_7
Luo, J., Liu, S.: Accelerating MUS enumeration by inconsistency graph partitioning. Sci. China Inf. Sci. 62(11), 1–11 (2019). https://doi.org/10.1007/s11432-019-9881-0
Mencía, C., Kullmann, O., Ignatiev, A., Marques-Silva, J.: On computing the union of MUSes. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 211–221. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_15
Bendík, J., Meel, K.S.: Approximate counting of minimal unsatisfiable subsets. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 439–462. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_21
Jaroslav, B., Cerna, I.: Rotation based MSS/MCS enumeration. In: Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 120–137. EasyChair, Alicante, Spain (2020)
Bendík, J., Černá, I.: MUST: minimal unsatisfiable subsets enumeration tool. TACAS 2020. LNCS, vol. 12078, pp. 135–152. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45190-5_8
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Zhang, J., Li, T., Ma, K. (2021). Accelerating Predicate Abstraction by Minimum Unsatisfiable Cores Extraction. In: He, K., Zhong, C., Cai, Z., Yin, Y. (eds) Theoretical Computer Science. NCTCS 2020. Communications in Computer and Information Science, vol 1352. Springer, Singapore. https://doi.org/10.1007/978-981-16-1877-2_1
Download citation
DOI: https://doi.org/10.1007/978-981-16-1877-2_1
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-16-1876-5
Online ISBN: 978-981-16-1877-2
eBook Packages: Computer ScienceComputer Science (R0)