A Simple yet Efficient MCSes Enumeration with SAT Oracles

Miyuki Koshimura; Ken Satoh

doi:10.1007/978-3-030-41964-6_17

A Simple yet Efficient MCSes Enumeration with SAT Oracles

Miyuki Koshimura, Ken Satoh

Intelligence Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Intelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings
Editors	Ngoc Thanh Nguyen, Bogdan Trawinski, Kietikul Jearanaitanakij, Suphamit Chittayasothorn, Ali Selamat
Publisher	Springer
Pages	191-201
Number of pages	11
ISBN (Print)	9783030419639
DOIs	https://doi.org/10.1007/978-3-030-41964-6_17
Publication status	Published - 2020
Event	12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020 - Phuket, Thailand Duration: Mar 23 2020 → Mar 26 2020

Publication series

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

Conference

Conference	12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020
Country/Territory	Thailand
City	Phuket
Period	3/23/20 → 3/26/20

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-030-41964-6_17

Cite this

Koshimura, M., & Satoh, K. (2020). A Simple yet Efficient MCSes Enumeration with SAT Oracles. In N. T. Nguyen, B. Trawinski, K. Jearanaitanakij, S. Chittayasothorn, & A. Selamat (Eds.), Intelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings (pp. 191-201). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12033 LNAI). Springer. https://doi.org/10.1007/978-3-030-41964-6_17

A Simple yet Efficient MCSes Enumeration with SAT Oracles. / Koshimura, Miyuki; Satoh, Ken.
Intelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings. ed. / Ngoc Thanh Nguyen; Bogdan Trawinski; Kietikul Jearanaitanakij; Suphamit Chittayasothorn; Ali Selamat. Springer, 2020. p. 191-201 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12033 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Koshimura, M & Satoh, K 2020, A Simple yet Efficient MCSes Enumeration with SAT Oracles. in NT Nguyen, B Trawinski, K Jearanaitanakij, S Chittayasothorn & A Selamat (eds), Intelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12033 LNAI, Springer, pp. 191-201, 12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020, Phuket, Thailand, 3/23/20. https://doi.org/10.1007/978-3-030-41964-6_17

Koshimura M, Satoh K. A Simple yet Efficient MCSes Enumeration with SAT Oracles. In Nguyen NT, Trawinski B, Jearanaitanakij K, Chittayasothorn S, Selamat A, editors, Intelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings. Springer. 2020. p. 191-201. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-41964-6_17

Koshimura, Miyuki ; Satoh, Ken. / A Simple yet Efficient MCSes Enumeration with SAT Oracles. Intelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings. editor / Ngoc Thanh Nguyen ; Bogdan Trawinski ; Kietikul Jearanaitanakij ; Suphamit Chittayasothorn ; Ali Selamat. Springer, 2020. pp. 191-201 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{8b3d1a144a1845e88f52893ba883fd69,

title = "A Simple yet Efficient MCSes Enumeration with SAT Oracles",

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.",

author = "Miyuki Koshimura and Ken Satoh",

note = "Funding Information: This work was supported by JSPS KAKENHI Grant Numbers JP17K00307 and JP19H04175. Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020 ; Conference date: 23-03-2020 Through 26-03-2020",

year = "2020",

doi = "10.1007/978-3-030-41964-6_17",

language = "English",

isbn = "9783030419639",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "191--201",

editor = "Nguyen, {Ngoc Thanh} and Bogdan Trawinski and Kietikul Jearanaitanakij and Suphamit Chittayasothorn and Ali Selamat",

booktitle = "Intelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings",

}

TY - GEN

T1 - A Simple yet Efficient MCSes Enumeration with SAT Oracles

AU - Koshimura, Miyuki

AU - Satoh, Ken

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85082308063&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85082308063&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-41964-6_17

DO - 10.1007/978-3-030-41964-6_17

M3 - Conference contribution

AN - SCOPUS:85082308063

SN - 9783030419639

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 191

EP - 201

BT - Intelligent Information and Database Systems - 12th Asian Conference, ACIIDS 2020, Proceedings

A2 - Nguyen, Ngoc Thanh

A2 - Trawinski, Bogdan

A2 - Jearanaitanakij, Kietikul

A2 - Chittayasothorn, Suphamit

A2 - Selamat, Ali

PB - Springer

T2 - 12th Asian Conference on Intelligent Information and Database Systems, ACIIDS 2020

Y2 - 23 March 2020 through 26 March 2020

ER -

A Simple yet Efficient MCSes Enumeration with SAT Oracles

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this