Towards Smarter MACE-style Model Finders
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Towards Smarter MACE-style Model Finders
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>ost</sub> - Miscellaneous article in a specialist periodical
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2018
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
EPiC Series in Computing
ISSN
2398-7340
e-ISSN
2398-7340
Volume of the periodical
8
Issue of the periodical within the volume
57
Country of publishing house
GB - UNITED KINGDOM
Number of pages
17
Pages from-to
454-470
UT code for WoS article
—
EID of the result in the Scopus database
—