Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Optimizing SMT Solving Strategies by Learning with an Evolutionary Process

Abstract :

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.

Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal.univ-angers.fr/hal-02715060
Contributeur : Okina Université d'Angers <>
Soumis le : lundi 1 juin 2020 - 19:56:44
Dernière modification le : mercredi 5 août 2020 - 03:48:34

Identifiants

  • HAL Id : hal-02715060, version 1
  • OKINA : ua17116

Citation

Nicolas Galvez Ramirez, Eric Monfroy, Frédéric Saubion, Carlos Castro. Optimizing SMT Solving Strategies by Learning with an Evolutionary Process. International Conference on High Performance Computing & Simulation : Pacos 2018, 2018, Orléans, France. ⟨hal-02715060⟩

Partager

Métriques

Consultations de la notice

26