BENDÍK, Jaroslav and Kuldeep S. MEEL. Counting Minimal Unsatisfiable Subsets. In Alexandra Silva, K. Rustan M. Leino. Computer Aided Verification - 33rd International Conference. Cham: Springer, 2021, p. 313-336. ISBN 978-3-030-81687-2. Available from: https://dx.doi.org/10.1007/978-3-030-81688-9_15.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Counting Minimal Unsatisfiable Subsets
Authors BENDÍK, Jaroslav (203 Czech Republic, guarantor, belonging to the institution) and Kuldeep S. MEEL (356 India).
Edition Cham, Computer Aided Verification - 33rd International Conference, p. 313-336, 24 pp. 2021.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Switzerland
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/21:00122309
Organization unit Faculty of Informatics
ISBN 978-3-030-81687-2
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-81688-9_15
UT WoS 000693429500015
Keywords in English satisfiability
Tags core_A, firank_1
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 26/4/2022 10:06.
Abstract
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.
PrintDisplayed: 19/7/2024 01:42