A Simple yet Efficient MCSes Enumeration with SAT Oracles

Miyuki Koshimura, Ken Satoh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The enumeration of the maximal satisfiable subsets (MSSes) or the minimal correction subsets (MCSes) of conjunctive normal form (CNF) formulas is a cornerstone task in various AI domains. This paper presents an algorithm that enumerates all MCSes with SAT oracles. Our algorithm is simple because it follows a plain algorithm without any techniques that decrease the number of calls to a SAT oracle. The experimental results show that our proposed method is more efficient than state-of-the-art MCS enumerators on average to deal with Partial-MaxSAT instances.

Original languageEnglish
Title of host publicationIntelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings
EditorsNgoc Thanh Nguyen, Bogdan Trawinski, Kietikul Jearanaitanakij, Suphamit Chittayasothorn, Ali Selamat
PublisherSpringer
Pages191-201
Number of pages11
ISBN (Print)9783030419639
DOIs
Publication statusPublished - 2020
Event12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020 - Phuket, Thailand
Duration: Mar 23 2020Mar 26 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12033 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020
CountryThailand
CityPhuket
Period3/23/203/26/20

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A Simple yet Efficient MCSes Enumeration with SAT Oracles'. Together they form a unique fingerprint.

Cite this