zbMATH — the first resource for mathematics

Exploiting symmetry in SMT problems. (English) Zbl 1341.68187
Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 222-236 (2011).
Summary: Methods exploiting problem symmetries have been very successful in several areas including constraint programming and SAT solving. We here recast a technique to enhance the performance of SMT-solvers by detecting symmetries in the input formulas and use them to prune the search space of the SMT algorithm. This technique is based on the concept of (syntactic) invariance by permutation of constants. An algorithm for solving SMT by taking advantage of such symmetries is presented. The implementation of this algorithm in the SMT-solver veriT is used to illustrate the practical benefits of this approach. It results in a significant improvement of veriT’s performances on the SMT-LIB benchmarks that places it ahead of the winners of the last editions of the SMT-COMP contest in the QF_UF category.
For the entire collection see [Zbl 1218.68006].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: DOI
[1] Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Peled, D., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 243–259. Springer, Heidelberg (2002) · Zbl 1037.68549 · doi:10.1007/3-540-36135-9_16
[2] Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability Modulo Theories Competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20–23. Springer, Heidelberg (2005) · Zbl 1081.68607 · doi:10.1007/11513988_4
[3] Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, ch.26, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009)
[4] Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Applied Logic 7(1), 58–74 (2009) · Zbl 1171.68040 · doi:10.1016/j.jal.2007.07.005
[5] Bouton, T., Caminha B. de Oliveira, D., Déharbe, D., Fontaine, P.: veriT: An open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 151–156. Springer, Heidelberg (2009) · Zbl 05587935 · doi:10.1007/978-3-642-02959-2_12
[6] Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic 52, 916–927 (1987) · Zbl 0636.03053 · doi:10.2307/2273826
[7] Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)
[8] Déharbe, D., Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploiting symmetry in SMT problems (2011), http://www.loria.fr/ fontaine/Deharbe6b.pdf · Zbl 1341.68187
[9] Gent, I.P., Petrie, K.E., Puget, J.-F.: Symmetry in Constraint Programming. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming. Foundations of Artificial Intelligence, vol. 2, pp. 329–376. Elsevier, Amsterdam (2006) · doi:10.1016/S1574-6526(06)80014-3
[10] Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297–308 (1985) · Zbl 0586.03010 · doi:10.1016/0304-3975(85)90144-6
[11] Jia, X., Zhang, J.: A powerful technique to eliminate isomorphism in finite model search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 318–331. Springer, Heidelberg (2006) · Zbl 1222.68365 · doi:10.1007/11814771_29
[12] Krishnamurthy, B.: Short proofs for tricky formulas. Acta Inf. 22, 253–275 (1985) · Zbl 0552.03009 · doi:10.1007/BF00265682
[13] Razborov, A.A.: Proof complexity of pigeonhole principles. In: Conference on Developments in Language Theory (DLT), pp. 100–116. Springer, Heidelberg (2002) · Zbl 1073.03540 · doi:10.1007/3-540-46011-X_8
[14] Roe, K.: The heuristic theorem prover: Yet another SMT modulo theorem prover. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 467–470. Springer, Heidelberg (2006) · Zbl 05187388 · doi:10.1007/11817963_42
[15] Sakallah, K.A.: Symmetry and satisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 289–338. IOS Press, Amsterdam (2009)
[16] Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 265–279. Springer, Heidelberg (2002) · Zbl 1010.68168 · doi:10.1007/3-540-45657-0_16
[17] Szeider, S.: The complexity of resolution with generalized symmetry rules. Theory Comput. Syst. 38(2), 171–188 (2005) · Zbl 1066.68121 · doi:10.1007/s00224-004-1192-0
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.