[Zurück]

B. Woltzenlogel-Paleo, P. Fontaine, S. Merz, D. Deharbe:
"Exploiting Symmetry in SMT Problems";
in: "Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings", Springer LNCS, LNCS/6803, 2011, ISBN: 978-3-642-22437-9, S. 222 - 236.

Methods exploiting problem symmetries have been very successful in several areas including constraint programming and SAT solving. We here present 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 taking advantage of such symmetries is presented. The implementation of this algorithm in the SMT-solver veriT is used to present the practical benefits of this approach. It results in a significant amelioration of veriT´s performances on the SMT-LIB benchmarks that place it ahead of the winners of the last editions of the SMT-COMP contest in the QF UF category.

Methods exploiting problem symmetries have been very successful in several areas including constraint programming and SAT solving. We here present 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 taking advantage of such symmetries is presented. The implementation of this algorithm in the SMT-solver veriT is used to present the practical benefits of this approach. It results in a significant amelioration of veriT´s performances on the SMT-LIB benchmarks that place it ahead of the winners of the last editions of the SMT-COMP contest in the QF UF category.

SMT-Solving, Sat-Solving, Symmetry Detection, Automated Theorem Proving

http://dx.doi.org/10.1007/978-3-642-22438-6_18

http://publik.tuwien.ac.at/files/PubDat_202131.pdf

Projektleitung Alexander Leitsch:
Beweistheoretische Anwendungen von CERES