Counting Maximal Satisfiable Subsets

D 2021

Counting Maximal Satisfiable Subsets

BENDÍK, Jaroslav a Kuldeep S. MEEL

Základní údaje

Originální název

Counting Maximal Satisfiable Subsets

Autoři

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

Vydání

Palo Alto, 35th AAAI Conference on Artificial Intelligence (AAAI-21), od s. 3651-3660, 10 s. 2021

Nakladatel

AAAI

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Kód RIV

RIV/00216224:14330/21:00120855

Organizační jednotka

Fakulta informatiky

ISBN

978-1-57735-866-4

ISSN

UT WoS

000680423503085

Klíčová slova anglicky

Constraint Satisfaction; Satisfiability; Diagnosis and Abductive Reasoning

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 15. 5. 2024 01:49, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Citovat

BENDÍK, Jaroslav a Kuldeep S. MEEL. Counting Maximal Satisfiable Subsets. Online. In 35th AAAI Conference on Artificial Intelligence (AAAI-21). Palo Alto: AAAI, 2021, s. 3651-3660. ISBN 978-1-57735-866-4.

@inproceedings{1706817,
   author = {Bendík, Jaroslav and Meel, Kuldeep S.},
   address = {Palo Alto},
   booktitle = {35th AAAI Conference on Artificial Intelligence (AAAI-21)},
   keywords = {Constraint Satisfaction; Satisfiability; Diagnosis and Abductive Reasoning},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Palo Alto},
   isbn = {978-1-57735-866-4},
   pages = {3651-3660},
   publisher = {AAAI},
   title = {Counting Maximal Satisfiable Subsets},
   url = {https://ojs.aaai.org/index.php/AAAI/article/view/16481},
   year = {2021}
}

TY  - JOUR
ID  - 1706817
AU  - Bendík, Jaroslav - Meel, Kuldeep S.
PY  - 2021
TI  - Counting Maximal Satisfiable Subsets
PB  - AAAI
CY  - Palo Alto
SN  - 9781577358664
KW  - Constraint Satisfaction
KW  - Satisfiability
KW  - Diagnosis and Abductive Reasoning
UR  - https://ojs.aaai.org/index.php/AAAI/article/view/16481
N2  - 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.
ER  -

BENDÍK, Jaroslav a Kuldeep S. MEEL. Counting Maximal Satisfiable Subsets. Online. In \textit{35th AAAI Conference on Artificial Intelligence (AAAI-21)}. Palo Alto: AAAI, 2021, s.~3651-3660. ISBN~978-1-57735-866-4.

Podrobný výpis o publikaci