Towards Learning Infinite SMT Models (Work in Progress)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F23%3A00380915" target="_blank" >RIV/68407700:21730/23:00380915 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1109/SYNASC61333.2023.00018" target="_blank" >https://doi.org/10.1109/SYNASC61333.2023.00018</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/SYNASC61333.2023.00018" target="_blank" >10.1109/SYNASC61333.2023.00018</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Towards Learning Infinite SMT Models (Work in Progress)

Popis výsledku v původním jazyce

This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of linear arithmetic with uninterpreted functions (UFLIA). The constructed models are piecewise linear. Such models are useful for satisfiable problems but also provide an alternative driver for model-based quantifier instantiation (MBQI).

Název v anglickém jazyce

Towards Learning Infinite SMT Models (Work in Progress)

Popis výsledku anglicky

This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of linear arithmetic with uninterpreted functions (UFLIA). The constructed models are piecewise linear. Such models are useful for satisfiable problems but also provide an alternative driver for model-based quantifier instantiation (MBQI).

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

<a href="/cs/project/LL1902" target="_blank" >LL1902: Obohacování SMT řešičů pomocí strojového učení</a><br>

Návaznosti

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

Rok uplatnění

2023

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

2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)

ISBN

979-8-3503-9413-9

ISSN

2470-8801

e-ISSN

2470-881X

Počet stran výsledku

4

Strana od-do

82-85

Název nakladatele

IEEE Industrial Electronic Society

Místo vydání

Vienna

Místo konání akce

Nancy

Datum konání akce

11. 9. 2023

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

WRD - Celosvětová akce

Kód UT WoS článku

001223988300024