Recursive Online Enumeration of All Minimal Unsatisfiable
Subsets

D 2018

Recursive Online Enumeration of All Minimal Unsatisfiable Subsets

BENDÍK, Jaroslav, Ivana ČERNÁ a Nikola BENEŠ

Základní údaje

Originální název

Recursive Online Enumeration of All Minimal Unsatisfiable Subsets

Autoři

BENDÍK, Jaroslav (203 Česká republika, garant, domácí), Ivana ČERNÁ (203 Česká republika, domácí) a Nikola BENEŠ (203 Česká republika, domácí)

Vydání

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

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/18:00101107

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-01089-8

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-01090-4_9

UT WoS

000723531300009

Klíčová slova anglicky

formal verification; minimal unstisfiable subsets

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 30. 4. 2019 07:25, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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

GA18-00178S, projekt VaV

Název: Diskrétní bifurkační analýza reaktivních systémů

Investor: Grantová agentura ČR, Diskrétní bifurkační analýza reaktivních systémů

MUNI/A/0854/2017, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/1038/2017, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BENDÍK, Jaroslav, Ivana ČERNÁ a Nikola BENEŠ. Recursive Online Enumeration of All Minimal Unsatisfiable Subsets. In Shuvendu Lahiri and Chao Wang. Automated Technology for Verification and Analysis - 16th International Symposium, {ATVA} 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings}. Los Angeles: Springer, 2018, s. 143-159. ISBN 978-3-030-01089-8. Dostupné z: https://dx.doi.org/10.1007/978-3-030-01090-4_9.

@inproceedings{1428840,
   author = {Bendík, Jaroslav and Černá, Ivana and Beneš, Nikola},
   address = {Los Angeles},
   booktitle = {Automated Technology for Verification and Analysis - 16th International Symposium, {ATVA} 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings}},
   doi = {http://dx.doi.org/10.1007/978-3-030-01090-4_9},
   editor = {Shuvendu Lahiri and Chao Wang},
   keywords = {formal verification; minimal unstisfiable subsets},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Los Angeles},
   isbn = {978-3-030-01089-8},
   pages = {143-159},
   publisher = {Springer},
   title = {Recursive Online Enumeration of All Minimal Unsatisfiable Subsets},
   url = {https://doi.org/10.1007/978-3-030-01090-4%5C_9},
   year = {2018}
}

TY  - JOUR
ID  - 1428840
AU  - Bendík, Jaroslav - Černá, Ivana - Beneš, Nikola
PY  - 2018
TI  - Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
PB  - Springer
CY  - Los Angeles
SN  - 9783030010898
KW  - formal verification
KW  - minimal unstisfiable subsets
UR  - https://doi.org/10.1007/978-3-030-01090-4%5C_9
N2  - 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.
ER  -

BENDÍK, Jaroslav, Ivana ČERNÁ a Nikola BENEŠ. Recursive Online Enumeration of All Minimal Unsatisfiable Subsets. In Shuvendu Lahiri and Chao Wang. \textit{Automated Technology for Verification and Analysis - 16th International Symposium, $\{$ATVA$\}$ 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings$\}$}. Los Angeles: Springer, 2018, s.~143-159. ISBN~978-3-030-01089-8. Dostupné z: https://dx.doi.org/10.1007/978-3-030-01090-4\_{}9.

Podrobný výpis o publikaci