Approximate Counting of Minimal Unsatisfiable Subsets

D 2020

Approximate Counting of Minimal Unsatisfiable Subsets

BENDÍK, Jaroslav a Kuldeep S. MEEL

Základní údaje

Originální název

Approximate Counting of Minimal Unsatisfiable Subsets

Autoři

BENDÍK, Jaroslav (203 Česká republika, garant, domácí) a Kuldeep S. MEEL (356 Indie)

Vydání

Neuveden, Computer Aided Verification - 32nd International Conference, CAV 2020, od s. 439-462, 24 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:00115568

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-53287-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-53288-8_21

UT WoS

000695276000021

Klíčová slova anglicky

minimal unsatisfiable subsets;MUS counting;diagnosis;metrics;knowledge base

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 16. 5. 2022 14:21, Mgr. Michal Petr

Anotace

V originále

Given an unsatisfiable formula F in CNF, i.e. a set of clauses, the problem of Minimal Unsatisfiable Subset (MUS) seeks to identify the minimal subset of clauses N subset F such that N is unsatisfiable. The emerging viewpoint of MUSes as the root causes of unsatisfiability has led MUSes to find applications in a wide variety of diagnostic approaches. Recent advances in finding and enumeration of MUSes have motivated researchers to discover applications that can benefit from rich information about the set of MUSes. One such extension is that of counting the number of MUSes, which has shown to describe the inconsistency metrics for general propositional knowledge bases. The current best approach for MUS counting is to employ a MUS enumeration algorithm, which often does not scale for the cases with a reasonably large number of MUSes. Motivated by the success of hashing-based techniques in the context of model counting, we design the first approximate counting procedure with (epsilon,delta) guarantees, called AMUSIC. Our approach avoids exhaustive MUS enumeration by combining the classical technique of universal hashing with advances in QBF solvers along with a novel usage of union and intersection of MUSes to achieve runtime efficiency. Our prototype implementation of AMUSIC is shown to scale to instances that were clearly beyond the reach of enumeration-based approaches.

Návaznosti

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 Kuldeep S. MEEL. Approximate Counting of Minimal Unsatisfiable Subsets. In Shuvendu K. Lahiri and Chao Wang. Computer Aided Verification - 32nd International Conference, CAV 2020. Neuveden: Springer, Cham, 2020, s. 439-462. ISBN 978-3-030-53287-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53288-8_21.

@inproceedings{1649416,
   author = {Bendík, Jaroslav and Meel, Kuldeep S.},
   address = {Neuveden},
   booktitle = {Computer Aided Verification - 32nd International Conference, CAV 2020},
   doi = {http://dx.doi.org/10.1007/978-3-030-53288-8_21},
   editor = {Shuvendu K. Lahiri and Chao Wang},
   keywords = {minimal unsatisfiable subsets;MUS counting;diagnosis;metrics;knowledge base},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-030-53287-1},
   pages = {439-462},
   publisher = {Springer, Cham},
   title = {Approximate Counting of Minimal Unsatisfiable Subsets},
   year = {2020}
}

TY  - JOUR
ID  - 1649416
AU  - Bendík, Jaroslav - Meel, Kuldeep S.
PY  - 2020
TI  - Approximate Counting of Minimal Unsatisfiable Subsets
PB  - Springer, Cham
CY  - Neuveden
SN  - 9783030532871
KW  - minimal unsatisfiable subsets;MUS counting;diagnosis;metrics;knowledge base
N2  - Given an unsatisfiable formula F in CNF, i.e. a set of clauses, the problem of Minimal Unsatisfiable Subset (MUS) seeks to identify the minimal subset of clauses N subset F such that N is unsatisfiable. The emerging viewpoint of MUSes as the root causes of unsatisfiability has led MUSes to find applications in a wide variety of diagnostic approaches. Recent advances in finding and enumeration of MUSes have motivated researchers to discover applications that can benefit from rich information about the set of MUSes. One such extension is that of counting the number of MUSes, which has shown to describe the inconsistency metrics for general propositional knowledge bases. The current best approach for MUS counting is to employ a MUS enumeration algorithm, which often does not scale for the cases with a reasonably large number of MUSes. Motivated by the success of hashing-based techniques in the context of model counting, we design the first approximate counting procedure with (epsilon,delta) guarantees, called AMUSIC. Our approach avoids exhaustive MUS enumeration by combining the classical technique of universal hashing with advances in QBF solvers along with a novel usage of union and intersection of MUSes to achieve runtime efficiency. Our prototype implementation of AMUSIC is shown to scale to instances that were clearly beyond the reach of enumeration-based approaches.
ER  -

BENDÍK, Jaroslav a Kuldeep S. MEEL. Approximate Counting of Minimal Unsatisfiable Subsets. In Shuvendu K. Lahiri and Chao Wang. \textit{Computer Aided Verification - 32nd International Conference, CAV 2020}. Neuveden: Springer, Cham, 2020, s.~439-462. ISBN~978-3-030-53287-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53288-8\_{}21.

Podrobný výpis o publikaci