Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.7
URN: urn:nbn:de:0030-drops-166810
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16681/
Janota, Mikoláš ; Piepenbrock, Jelle ; Piotrowski, Bartosz
Towards Learning Quantifier Instantiation in SMT
| pdf-format: |
|
Abstract
This paper applies machine learning (ML) to solve quantified satisfiability modulo theories (SMT) problems more efficiently. The motivating idea is that the solver should learn from already solved formulas to solve new ones. This is especially relevant in classes of similar formulas.We focus on the enumerative instantiation - a well-established approach to solving quantified formulas anchored in the Herbrand’s theorem. The task is to select the right ground terms to be instantiated. In ML parlance, this means learning to rank ground terms. We devise a series of features of the considered terms and train on them using boosted decision trees. In particular, we integrate the LightGBM library into the SMT solver cvc5. The experimental results demonstrate that the ML-guided solver enables us to solve more formulas than the base solver and reduce the number of quantifier instantiations. We also do an ablation study on the features used in the machine learning component, showing the contributions of the various additions.
BibTeX - Entry
@InProceedings{janota_et_al:LIPIcs.SAT.2022.7,
author = {Janota, Mikol\'{a}\v{s} and Piepenbrock, Jelle and Piotrowski, Bartosz},
title = {{Towards Learning Quantifier Instantiation in SMT}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16681},
URN = {urn:nbn:de:0030-drops-166810},
doi = {10.4230/LIPIcs.SAT.2022.7},
annote = {Keywords: satisfiability modulo theories, quantifier instantiation, machine learning}
}
| Keywords: | satisfiability modulo theories, quantifier instantiation, machine learning | |
| Seminar: | 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 28.07.2022 |
