Towards Learning Quantifier Instantiation in SMT

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Towards Learning Quantifier Instantiation in SMT

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2022

Confidentiality

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

Article name in the collection

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

ISBN

978-3-95977-242-6

ISSN

—

e-ISSN

1868-8969

Number of pages

18

Pages from-to

—

Publisher name

Dagstuhl Publishing,

Place of publication

Saarbrücken

Event location

Haifa

Event date

Aug 2, 2022

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—