Towards Smarter MACE-style Model Finders

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F18%3A00329607" target="_blank" >RIV/68407700:21730/18:00329607 - isvavai.cz</a>

Výsledek na webu

<a href="https://easychair.org/publications/paper/rZKt" target="_blank" >https://easychair.org/publications/paper/rZKt</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/w42s" target="_blank" >10.29007/w42s</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Towards Smarter MACE-style Model Finders

Popis výsledku v původním jazyce

Finite model finders represent a powerful tool for deciding problems with the finite model property, such as the Bernays-Schonfinkel fragment (EPR). Further, finite model finders provide useful information for counter-satisfiable conjectures. The paper investigates several novel techniques in a finite model-_nder based on the translation to SAT, referred to as the MACE-style approach. The approach we propose is driven by counterexample abstraction refinement (CEGAR), which has proven to be a powerful tool in the context of quantifiers in satisfiability modulo theories (SMT) and quantified Boolean formulas (QBF). One weakness of CEGAR-based approaches is that certain amount of luck is required in order to guess the right model, because the solver always operates on incomplete information about the formula. To tackle this issue, we propose to enhance the model finder with a machine learning algorithm to improve the likelihood that the right model is encountered. The implemented prototype based on the presented ideas shows highly promising results.

Název v anglickém jazyce

Towards Smarter MACE-style Model Finders

Popis výsledku anglicky

Finite model finders represent a powerful tool for deciding problems with the finite model property, such as the Bernays-Schonfinkel fragment (EPR). Further, finite model finders provide useful information for counter-satisfiable conjectures. The paper investigates several novel techniques in a finite model-_nder based on the translation to SAT, referred to as the MACE-style approach. The approach we propose is driven by counterexample abstraction refinement (CEGAR), which has proven to be a powerful tool in the context of quantifiers in satisfiability modulo theories (SMT) and quantified Boolean formulas (QBF). One weakness of CEGAR-based approaches is that certain amount of luck is required in order to guess the right model, because the solver always operates on incomplete information about the formula. To tackle this issue, we propose to enhance the model finder with a machine learning algorithm to improve the likelihood that the right model is encountered. The implemented prototype based on the presented ideas shows highly promising results.

Druh

J_ost - Ostatní články v recenzovaných periodicích

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/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>

Návaznosti

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

Rok uplatnění

2018

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 periodika

EPiC Series in Computing

ISSN

2398-7340

e-ISSN

2398-7340

Svazek periodika

8

Číslo periodika v rámci svazku

57

Stát vydavatele periodika

GB - Spojené království Velké Británie a Severního Irska

Počet stran výsledku

17

Strana od-do

454-470

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—