Counting Maximal Satisfiable Subsets

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F21%3A00120855" target="_blank" >RIV/00216224:14330/21:00120855 - isvavai.cz</a>

Result on the web

<a href="https://ojs.aaai.org/index.php/AAAI/article/view/16481" target="_blank" >https://ojs.aaai.org/index.php/AAAI/article/view/16481</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Counting Maximal Satisfiable Subsets

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2021

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

35th AAAI Conference on Artificial Intelligence (AAAI-21)

ISBN

9781577358664

ISSN

2159-5399

e-ISSN

2374-3468

Number of pages

10

Pages from-to

3651-3660

Publisher name

AAAI

Place of publication

Palo Alto

Event location

Palo Alto

Event date

Jan 1, 2021

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000680423503085