Replication-Guided Enumeration of Minimal Unsatisfiable Subsets

D 2020

Replication-Guided Enumeration of Minimal Unsatisfiable Subsets

BENDÍK, Jaroslav a Ivana ČERNÁ

Základní údaje

Originální název

Replication-Guided Enumeration of Minimal Unsatisfiable Subsets

Autoři

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

Vydání

Neuveden, 26th International Conference on Principles and Practice of Constraint Programming, od s. 37-54, 18 s. 2020

Nakladatel

Springer, Cham

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"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00116179

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-58474-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-58475-7_3

Klíčová slova anglicky

Minimal Unsatisfiable Subsets;MUSes;Over-constrained systems

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 10. 5. 2021 05:51, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

In many areas of computer science, we are given an unsatisfiable Boolean formula F in CNF, i.e. a set of clauses, with the goal to identify minimal unsatisfiable subsets (MUSes) of F. The more MUSes are identified, the better insight into F’s unsatisfiability is obtained. Unfortunately, finding even a single MUS can be very time consuming since it naturally subsumes repeatedly solving the satisfiability problem, and thus a complete MUS enumeration is often practically intractable. Therefore, contemporary MUS enumeration algorithms tend to identify as many MUSes as possible within a given time limit. In this work, we present a novel MUS enumeration algorithm. Compared to existing algorithms, our algorithm is much more frugal in the number of performed satisfiability checks. Consequently, our algorithm is often able to find substantially more MUSes than contemporary algorithms.

Návaznosti

EF16_019/0000822, projekt VaV

Název: Centrum excelence pro kyberkriminalitu, kyberbezpečnost a ochranu kritických informačních infrastruktur

MUNI/A/1050/2019, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Akronym: SV-FI MAV IX)

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

MUNI/A/1076/2019, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Akronym: SKOMU)

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

Citovat

BENDÍK, Jaroslav a Ivana ČERNÁ. Replication-Guided Enumeration of Minimal Unsatisfiable Subsets. In Helmut Simonis. 26th International Conference on Principles and Practice of Constraint Programming. Neuveden: Springer, Cham, 2020, s. 37-54. ISBN 978-3-030-58474-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-58475-7_3.

@inproceedings{1673818,
   author = {Bendík, Jaroslav and Černá, Ivana},
   address = {Neuveden},
   booktitle = {26th International Conference on Principles and Practice of Constraint Programming},
   doi = {http://dx.doi.org/10.1007/978-3-030-58475-7_3},
   editor = {Helmut Simonis},
   keywords = {Minimal Unsatisfiable Subsets;MUSes;Over-constrained systems},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-030-58474-0},
   pages = {37-54},
   publisher = {Springer, Cham},
   title = {Replication-Guided Enumeration of Minimal Unsatisfiable Subsets},
   year = {2020}
}

TY  - JOUR
ID  - 1673818
AU  - Bendík, Jaroslav - Černá, Ivana
PY  - 2020
TI  - Replication-Guided Enumeration of Minimal Unsatisfiable Subsets
PB  - Springer, Cham
CY  - Neuveden
SN  - 9783030584740
KW  - Minimal Unsatisfiable Subsets;MUSes;Over-constrained systems
N2  - In many areas of computer science, we are given an unsatisfiable Boolean formula F in CNF, i.e. a set of clauses, with the goal to identify minimal unsatisfiable subsets (MUSes) of F. The more MUSes are identified, the better insight into F’s unsatisfiability is obtained. Unfortunately, finding even a single MUS can be very time consuming since it naturally subsumes repeatedly solving the satisfiability problem, and thus a complete MUS enumeration is often practically intractable. Therefore, contemporary MUS enumeration algorithms tend to identify as many MUSes as possible within a given time limit. In this work, we present a novel MUS enumeration algorithm. Compared to existing algorithms, our algorithm is much more frugal in the number of performed satisfiability checks. Consequently, our algorithm is often able to find substantially more MUSes than contemporary algorithms.
ER  -

BENDÍK, Jaroslav a Ivana ČERNÁ. Replication-Guided Enumeration of Minimal Unsatisfiable Subsets. In Helmut Simonis. \textit{26th International Conference on Principles and Practice of Constraint Programming}. Neuveden: Springer, Cham, 2020, s.~37-54. ISBN~978-3-030-58474-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-58475-7\_{}3.

Podrobný výpis o publikaci