Towards Learning Quantifier Instantiation in SMT

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F22%3A00364128" target="_blank" >RIV/68407700:21730/22:00364128 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.4230/LIPIcs.SAT.2022.7" target="_blank" >https://doi.org/10.4230/LIPIcs.SAT.2022.7</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.SAT.2022.7" target="_blank" >10.4230/LIPIcs.SAT.2022.7</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Towards Learning Quantifier Instantiation in SMT

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Towards Learning Quantifier Instantiation in SMT

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

ISBN

978-3-95977-242-6

ISSN

—

e-ISSN

1868-8969

Počet stran výsledku

18

Strana od-do

—

Název nakladatele

Dagstuhl Publishing,

Místo vydání

Saarbrücken

Místo konání akce

Haifa

Datum konání akce

2. 8. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—