Contributions to Proceedings:
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,
222
- 236.
English abstract:
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.
German abstract:
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.
Keywords:
SMT-Solving, Sat-Solving, Symmetry Detection, Automated Theorem Proving
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-642-22438-6_18
Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_202131.pdf
Related Projects:
Project Head Alexander Leitsch:
Beweistheoretische Anwendungen von CERES
Created from the Publication Database of the Vienna University of Technology.