<div class="csl-bib-body">
<div class="csl-entry">Bendik, J. (2021). On Decomposition of Maximal Satisfiable Subsets. In <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021</i> (pp. 212–221). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_30</div>
</div>
In many areas of computer science, we are given an
unsatisfiable formula F in CNF, i.e., a set of clauses, with the
goal to analyze the unsatisfiability. A kind of such analysis is to
identify Minimal Correction Subsets (MCSes) of F, i.e., minimal
subsets of clauses that need to be removed from F to make it
satisfiable. Equivalently, one might identify the complements of
MCSes, i.e., Maximal Satisfiable Subsets (MSSes) of F. The more
MSSes (MCSes) of F are identified, the better insight into the unsatisfiability
can be obtained. Hence, there were proposed many
algorithms for complete MSS (MCS) enumeration. Unfortunately,
the number of MSSes can be exponential w.r.t. |F|, which often
makes the complete enumeration practically intractable.
In this work, we attempt to cope with the intractability of
complete MSS enumeration by initiating the study on MSS
decomposition. In particular, we propose several techniques that
often allows for decomposing the input formula F into several
subformulas. Subsequently, we explicitly enumerate all MSSes
of the subformulas, and then combine those MSSes to form
MSSes of the original formula F. An extensive empirical study
demonstrates that due to the MSS decomposition, the number of
MSSes that need to be explicitly identified is often exponentially
smaller than the total number of MSSes. Consequently, we
are able to improve upon a scalability of contemporary MSS
enumeration approaches by many orders of magnitude.
en
dc.language.iso
en
-
dc.relation.ispartofseries
Conference Series: Formal Methods in Computer-Aided Design
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
formal methods
en
dc.subject
computer-aided system design
en
dc.subject
hardware and system verification
en
dc.subject
formale Methode
de
dc.subject
rechnerunterstützte Systementwicklung
de
dc.subject
Hardwareverifikation
de
dc.title
On Decomposition of Maximal Satisfiable Subsets
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34727/2021/isbn.978-3-85448-046-4_30
-
dc.contributor.affiliation
Max Planck Institute for Software Systems, Deutschland
-
dc.relation.isbn
978-3-85448-046-4
-
dc.relation.doi
10.34727/2021/isbn.978-3-85448-046-4
-
dc.description.volume
2
-
dc.description.startpage
212
-
dc.description.endpage
221
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
2708-7824
-
tuw.booktitle
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
-
tuw.peerreviewed
true
-
tuw.relation.haspart
10.34727/2021/isbn.978-3-85448-046-4
-
tuw.relation.publisher
TU Wien Academic Press
-
tuw.relation.publisherplace
Wien
-
tuw.book.chapter
30
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
dc.description.numberOfPages
10
-
tuw.relation.ispartoftuwseries
Conference Series: Formal Methods in Computer-Aided Design
-
tuw.author.orcid
0000-0001-9784-3028
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
item.cerifentitytype
Publications
-
item.openaccessfulltext
Open Access
-
item.fulltext
with Fulltext
-
item.languageiso639-1
en
-
item.grantfulltext
open
-
item.openairetype
conference paper
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.mimetype
application/pdf
-
crisitem.author.dept
Max Planck Institute for Software Systems, Deutschland