Symmetry Avoidance in MACE-Style Finite Model Finding

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Symmetry Avoidance in MACE-Style Finite Model Finding

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Symmetry Avoidance in MACE-Style Finite Model Finding

Popis výsledku anglicky

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.

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

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2019

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

Frontiers of Combining Systems.

ISBN

978-3-030-29006-1

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

19

Strana od-do

3-21

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

London

Datum konání akce

4. 9. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

000611607300001