A Simple yet Efficient MCSes Enumeration with SAT Oracles

Miyuki Koshimura, Ken Satoh

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

抄録

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.

本文言語英語
ホスト出版物のタイトルIntelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings
編集者Ngoc Thanh Nguyen, Bogdan Trawinski, Kietikul Jearanaitanakij, Suphamit Chittayasothorn, Ali Selamat
出版社Springer
ページ191-201
ページ数11
ISBN(印刷版)9783030419639
DOI
出版ステータス出版済み - 2020
イベント12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020 - Phuket, タイ
継続期間: 3 23 20203 26 2020

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
12033 LNAI
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

会議

会議12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020
Countryタイ
CityPhuket
Period3/23/203/26/20

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「A Simple yet Efficient MCSes Enumeration with SAT Oracles」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル