Symmetry Avoidance in MACE-Style Finite Model Finding
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F19%3A00339882" target="_blank" >RIV/68407700:21730/19:00339882 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/978-3-030-29007-8_1" target="_blank" >https://doi.org/10.1007/978-3-030-29007-8_1</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-29007-8_1" target="_blank" >10.1007/978-3-030-29007-8_1</a>
Alternative languages
Result language
angličtina
Original language name
Symmetry Avoidance in MACE-Style Finite Model Finding
Original language description
This work considers the MACE-style approach to finite model finding for (multi-sorted) first-order logic. This existing approach iteratively assumes increasing domain sizes and encodes the corresponding model existence problem as a SAT problem. The original MACE tool and its successors have considered techniques for avoiding introducing symmetries in the resulting SAT problem, but this has never been the focus of the previous work and has not received concentrated attention. In this work we formalise the symmetry avoiding problem, characterise the notion of a sound symmetry breaking heuristic, propose a number of such heuristics and evaluate them experimentally with an implementation in the Vampire theorem prover. Our results demonstrate that these new heuristics improve performance on a number of benchmarks taken from SMT-LIB and TPTP. Finally, we show that direct symmetry breaking techniques could be used to improve finite model finding, but that their cost means that symmetry avoidance is still the preferable approach.
Czech name
—
Czech description
—
Classification
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)
Result continuities
Project
—
Continuities
R - Projekt Ramcoveho programu EK
Others
Publication year
2019
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
Article name in the collection
Frontiers of Combining Systems.
ISBN
978-3-030-29006-1
ISSN
0302-9743
e-ISSN
—
Number of pages
19
Pages from-to
3-21
Publisher name
Springer
Place of publication
Cham
Event location
London
Event date
Sep 4, 2019
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000611607300001