Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-030-81688-9_15
Title: Counting Minimal Unsatisfiable Subsets
Authors: Bendík, J. 
Meel, Kuldeep S.
Issue Date: 1-Jan-2021
Publisher: Springer Science and Business Media Deutschland GmbH
Citation: Bendík, J., Meel, Kuldeep S. (2021-01-01). Counting Minimal Unsatisfiable Subsets. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 12760 LNCS : 313-336. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-030-81688-9_15
Rights: Attribution 4.0 International
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, Bendík 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. © 2021, The Author(s).
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: https://scholarbank.nus.edu.sg/handle/10635/233330
ISBN: 9783030816872
ISSN: 0302-9743
DOI: 10.1007/978-3-030-81688-9_15
Rights: Attribution 4.0 International
Appears in Collections:Staff Publications
Elements

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
10_1007_978-3-030-81688-9_15.pdf682.4 kBAdobe PDF

OPEN

NoneView/Download

SCOPUSTM   
Citations

1
checked on Jan 22, 2023

Page view(s)

18
checked on Jan 26, 2023

Google ScholarTM

Check

Altmetric


This item is licensed under a Creative Commons License Creative Commons