Recursive Online Enumeration of All Minimal Unsatisfiable Subsets

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F18%3A00101107" target="_blank" >RIV/00216224:14330/18:00101107 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-01090-4_9" target="_blank" >http://dx.doi.org/10.1007/978-3-030-01090-4_9</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-01090-4_9" target="_blank" >10.1007/978-3-030-01090-4_9</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Recursive Online Enumeration of All Minimal Unsatisfiable Subsets

Popis výsledku v původním jazyce

In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such cores are called minimal unsatisfiable subsets (MUSes). The more MUSes are identified, the more information about the conflicts among the constraints is obtained. However, a full enumeration of all MUSes is in general intractable due to the large number (even exponential) of possible conflicts. Moreover, to identify MUSes, algorithms have to test sets of constraints for their simultaneous satisfiability. The type of the test depends on the application domains. The complexity of the tests can be extremely high especially for domains like temporal logics, model checking, or SMT. In this paper, we propose a recursive algorithm that identifies MUSes in an online manner (i.e., one by one) and can be terminated at any time. The key feature of our algorithm is that it minimises the number of satisfiability tests and thus speeds up the computation. The algorithm is applicable to an arbitrary constraint domain and proves to be efficient especially in domains with expensive satisfiability checks. We benchmark our algorithm against the state-of-the-art algorithm Marco on the Boolean and SMT constraint domains and demonstrate that our algorithm really requires less satisfiability tests and consequently finds more MUSes in the given time limits.

Název v anglickém jazyce

Recursive Online Enumeration of All Minimal Unsatisfiable Subsets

Popis výsledku anglicky

In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such cores are called minimal unsatisfiable subsets (MUSes). The more MUSes are identified, the more information about the conflicts among the constraints is obtained. However, a full enumeration of all MUSes is in general intractable due to the large number (even exponential) of possible conflicts. Moreover, to identify MUSes, algorithms have to test sets of constraints for their simultaneous satisfiability. The type of the test depends on the application domains. The complexity of the tests can be extremely high especially for domains like temporal logics, model checking, or SMT. In this paper, we propose a recursive algorithm that identifies MUSes in an online manner (i.e., one by one) and can be terminated at any time. The key feature of our algorithm is that it minimises the number of satisfiability tests and thus speeds up the computation. The algorithm is applicable to an arbitrary constraint domain and proves to be efficient especially in domains with expensive satisfiability checks. We benchmark our algorithm against the state-of-the-art algorithm Marco on the Boolean and SMT constraint domains and demonstrate that our algorithm really requires less satisfiability tests and consequently finds more MUSes in the given time limits.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

<a href="/cs/project/GA18-00178S" target="_blank" >GA18-00178S: Diskrétní bifurkační analýza reaktivních systémů</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 statě ve sborníku

Automated Technology for Verification and Analysis - 16th International Symposium, {ATVA} 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings}

ISBN

9783030010898

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

17

Strana od-do

143-159

Název nakladatele

Springer

Místo vydání

Los Angeles

Místo konání akce

Los Angeles

Datum konání akce

1. 1. 2018

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

WRD - Celosvětová akce

Kód UT WoS článku

000723531300009