Counting Minimal Unsatisfiable Subsets

D 2021

Counting Minimal Unsatisfiable Subsets

BENDÍK, Jaroslav a Kuldeep S. MEEL

Základní údaje

Originální název

Counting Minimal Unsatisfiable Subsets

Autoři

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

Vydání

Cham, Computer Aided Verification - 33rd International Conference, od s. 313-336, 24 s. 2021

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

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/21:00122309

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-81687-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-81688-9_15

UT WoS

000693429500015

Klíčová slova anglicky

satisfiability

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 26. 4. 2022 10:06, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Given an unsatisfiable Boolean formula F in CNF, an unsatisfiable subset of clauses U of F is called Minimal Unsatisfiable Subset (MUS) if every proper subset of U is satisfiable. Since MUSes serve as explanations for the unsatisfiability of F, MUSes find applications in a wide variety of domains. The availability of efficient SAT solvers has aided the development of scalable techniques for finding and enumerating MUSes in the past two decades. Building on the recent developments in the design of scalable model counting techniques for SAT, Bendik and Meel initiated the study of MUS counting techniques. They succeeded in designing the first approximate MUS counter, AMUSIC, that does not rely on exhaustive MUS enumeration. AMUSIC, however, suffers from two shortcomings: the lack of exact estimates and limited scalability due to its reliance on 3-QBF solvers. In this work, we address the two shortcomings of AMUSIC by designing the first exact MUS counter, CountMUST, that does not rely on exhaustive enumeration. CountMUST circumvents the need for 3-QBF solvers by reducing the problem of MUS counting to projected model counting. While projected model counting is #NP-hard, the past few years have witnessed the development of scalable projected model counters. An extensive empirical evaluation demonstrates that CountMUST successfully returns MUS count for 1500 instances while AMUSIC and enumeration-based techniques could only handle up to 833 instances.

Citovat

BENDÍK, Jaroslav a Kuldeep S. MEEL. Counting Minimal Unsatisfiable Subsets. In Alexandra Silva, K. Rustan M. Leino. Computer Aided Verification - 33rd International Conference. Cham: Springer, 2021, s. 313-336. ISBN 978-3-030-81687-2. Dostupné z: https://dx.doi.org/10.1007/978-3-030-81688-9_15.

@inproceedings{1790958,
   author = {Bendík, Jaroslav and Meel, Kuldeep S.},
   address = {Cham},
   booktitle = {Computer Aided Verification - 33rd International Conference},
   doi = {http://dx.doi.org/10.1007/978-3-030-81688-9_15},
   editor = {Alexandra Silva, K. Rustan M. Leino},
   keywords = {satisfiability},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-81687-2},
   pages = {313-336},
   publisher = {Springer},
   title = {Counting Minimal Unsatisfiable Subsets},
   year = {2021}
}

TY  - JOUR
ID  - 1790958
AU  - Bendík, Jaroslav - Meel, Kuldeep S.
PY  - 2021
TI  - Counting Minimal Unsatisfiable Subsets
PB  - Springer
CY  - Cham
SN  - 9783030816872
KW  - satisfiability
N2  - Given an unsatisfiable Boolean formula F in CNF, an unsatisfiable subset of clauses U of F is called Minimal Unsatisfiable Subset (MUS) if every proper subset of U is satisfiable. Since MUSes serve as explanations for the unsatisfiability of F, MUSes find applications in a wide variety of domains. The availability of efficient SAT solvers has aided the development of scalable techniques for finding and enumerating MUSes in the past two decades. Building on the recent developments in the design of scalable model counting techniques for SAT, Bendik and Meel initiated the study of MUS counting techniques. They succeeded in designing the first approximate MUS counter, AMUSIC, that does not rely on exhaustive MUS enumeration. AMUSIC, however, suffers from two shortcomings: the lack of exact estimates and limited scalability due to its reliance on 3-QBF solvers. In this work, we address the two shortcomings of AMUSIC by designing the first exact MUS counter, CountMUST, that does not rely on exhaustive enumeration. CountMUST circumvents the need for 3-QBF solvers by reducing the problem of MUS counting to projected model counting. While projected model counting is #NP-hard, the past few years have witnessed the development of scalable projected model counters. An extensive empirical evaluation demonstrates that CountMUST successfully returns MUS count for 1500 instances while AMUSIC and enumeration-based techniques could only handle up to 833 instances.
ER  -

BENDÍK, Jaroslav a Kuldeep S. MEEL. Counting Minimal Unsatisfiable Subsets. In Alexandra Silva, K. Rustan M. Leino. \textit{Computer Aided Verification - 33rd International Conference}. Cham: Springer, 2021, s.~313-336. ISBN~978-3-030-81687-2. Dostupné z: https://dx.doi.org/10.1007/978-3-030-81688-9\_{}15.

Podrobný výpis o publikaci