Optimizing SMT Solving Strategies by Learning with an Evolutionary Process
| Autor: | Carlos Castro, Nicolas Galvez Ramirez, Eric Monfroy, Frédéric Saubion |
|---|---|
| Přispěvatelé: | Laboratoire d'Etudes et de Recherche en Informatique d'Angers (LERIA), Université d'Angers (UA), Universidad Tecnica Federico Santa Maria [Valparaiso] (UTFSM), Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
business.industry
Process (engineering) Computer science Modulo Evolutionary algorithm Genetic programming 02 engineering and technology Program optimization Solver Machine learning computer.software_genre Evolutionary computation Satisfiability modulo theories 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing [INFO]Computer Science [cs] Artificial intelligence business computer |
| Zdroj: | International Conference on High Performance Computing & Simulation : Pacos 2018 International Conference on High Performance Computing & Simulation : Pacos 2018, 2018, Orléans, France HPCS |
| Popis: | This paper deals with program optimization, i.e., learning of more efficient programs. The programs we want to improve are Z3 solving strategies. Z3 is a SMT (SAT Modulo Theory) solver which is currently developed by Microsoft Research. We define strategy generators based on evolutionary processes. SMT solving strategies include various aspects that can affect the performance of a SMT solver dramatically. Each of these elements includes a huge amount of options which cannot be exploited without expert knowledge. We define a generic evolutionary algorithm based on genetic programming concepts. This strategy generation process aims at learning better strategies by successive improvements, using rules that can be combined in order to handle both structures and parameters of the strategies. We experiment 7 different strategies generators on 2 SMT logics (QF_LRA,QF_LIA). The results show that the learned strategies improve default strategies available in the solver. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|