BENDÍK, Jaroslav and Kuldeep S. MEEL. Counting Maximal Satisfiable Subsets. Online. In 35th AAAI Conference on Artificial Intelligence (AAAI-21). Palo Alto: AAAI, 2021. p. 3651-3660. ISBN 978-1-57735-866-4. [citováno 2024-04-24]
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Counting Maximal Satisfiable Subsets
Authors BENDÍK, Jaroslav (203 Czech Republic, guarantor, belonging to the institution) and Kuldeep S. MEEL (356 India)
Edition Palo Alto, 35th AAAI Conference on Artificial Intelligence (AAAI-21), p. 3651-3660, 10 pp. 2021.
Publisher AAAI
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW URL
RIV identification code RIV/00216224:14330/21:00120855
Organization unit Faculty of Informatics
ISBN 978-1-57735-866-4
ISSN 2159-5399
UT WoS 000680423503085
Keywords in English Constraint Satisfaction; Satisfiability; Diagnosis and Abductive Reasoning
Tags core_A, firank_1
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 25/4/2022 16:48.
Abstract
Given an unsatisfiable set of constraints F, a maximal satisfiable subset (MSS) is a maximal subset of constraints C ⊆ F such that C is satisfiable. Over the past two decades, the steady improvement in runtime performance of algorithms for finding MSS has led to an increased adoption of MSS-based techniques in wide variety of domains. Motivated by the progress in finding an MSS, the past decade has witnessed a surge of interest in design of algorithmic techniques to enumerate all the MSSes, which has subsequently led to discovery of new applications utilizing enumeration of MSSes. The development of techniques for finding and enumeration of MSSes mirrors a similar phenomenon of finding and enumeration of SAT solutions in the early 2000s, which subsequently motivated design of algorithmic techniques for model counting. In a similar spirit, we undertake study to investigate the feasibility of MSS counting techniques. In particular, the focus point of our investigation is to answer whether one can design efficient MSS counting techniques that do not rely on explicit MSS enumeration. The primary contribution of this work is an affirmative answer to the above question. Our tool, CountMSS, uses a novel architecture of a wrapper W and a remainder R such that the desired MSS count can be expressed as |W| − |R|. CountMSS relies on the advances in projected model counting to efficiently compute |W| and |R|. Our empirical evaluation demonstrates that CountMSS is able to scale to instances clearly beyond the reach of enumeration-based techniques.
PrintDisplayed: 24/4/2024 06:01