Towards Automated Strategies in Satisfiability Modulo Theory
SMT solvers include many heuristic components in order to ease the theorem proving process for different logics and problems. Handling these heuristics is a non-trivial task requiring specific knowledge of many theories that even a SMT solver developer may be unaware of. This is the first barrier to break in order to allow end-users to control heuristics aspects of any SMT solver and to successfully build a strategy for their own purposes. We present a first attempt for generating an automatic selection of heuristics in order to improve SMT solver efficiency and to allow end-users to take better advantage of solvers when unknown problems are faced. Evidence of improvement is shown and the basis for future works with evolutionary and/or learning-based algorithms are raised.
KeywordsSMT Strategy Z3 Learning Tuning Evolutionary algorithm Search-based software engineering
We want to thanks Christopher Wintersteiger from Microsoft Research for provide us critical information about Z3 theorem prover. Nicolás Gálvez Ramírez is granted by Chilean government: CONICYT-PCHA / Doctorado Nacional / 2013-21130089.
- 1.Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). www.SMT-LIB.org
- 3.Gálvez Ramírez, N., Hamadi, Y., Monfroy, E., Saubion, F.: Towards Automated Strategies in Satisfiability Modulo Theory: Appendix. http://www.inf.utfsm.cl/~ngalvez/strategies.pdf
- 6.Harman, M.: The role of Artificial Intelligence in Software Engineering. In: 2012 First International Workshop on Realizing Artificial Intelligence Synergies in Software Engineering (RAISE), pp. 1–6 (2012)Google Scholar
- 10.Nannen, V., Eiben, A.: Efficient relevance estimation and value calibration of evolutionary algorithm parameters. In: IEEE Congress on Evolutionary Computation, CEC, pp. 103–110 (2007)Google Scholar
- 12.Riff, M.C., Montero, E.: A new algorithm for reducing metaheuristic design effort. In: 2013 IEEE Congress on Evolutionary Computation (CEC), pp. 3283–3290, June 2013Google Scholar
- 13.SMT-LIB Community: SMT-LIB Logics, Accessed 10 September 2015. http://smtlib.cs.uiowa.edu/logics.shtml