Counting Minimal Unsatisfiable Subsets

Result code in IS VaVaI

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

Result on the web

<a href="http://dx.doi.org/10.1007/978-3-030-81688-9_15" target="_blank" >http://dx.doi.org/10.1007/978-3-030-81688-9_15</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-81688-9_15" target="_blank" >10.1007/978-3-030-81688-9_15</a>

Result language

angličtina

Original language name

Counting Minimal Unsatisfiable Subsets

Original language description

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.

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

Computer Aided Verification - 33rd International Conference

ISBN

9783030816872

ISSN

0302-9743

e-ISSN

1611-3349

Number of pages

24

Pages from-to

313-336

Publisher name

Springer

Place of publication

Cham

Event location

Cham

Event date

Jan 1, 2021

Type of event by nationality

CST - Celostátní akce

UT code for WoS article

000693429500015