[1E2-OS-3a] AI における離散構造処理と制約充足(1)

[1E2-OS-3a-02] MCSes Enumeration with the Glucose SAT Solver

〇Miyuki Koshimura¹, Ken Satoh² (1. Kyushu University, 2. National Institute of Informatics)

Keywords:SAT, MCSes Enumeration

Enumerating all Maximal Satisfiable Subsets (MSSes) or all Minimal
Correction Subsets (MCSes) of an unsatisfiable CNF Boolean formula is
a cornerstone task in various AI domains. This paper considers MCSes
enumeration with a SAT solver. We aim to develop a procedure which
outperforms several MCSes enumerators proposed so far.

The paper presents a basic enumeration procedure and compares it with
a state-of-the-art enumerator Enum-ELS-RMR-Cache. The
experimental results show that the proposed procedure is more
efficient than Enum-ELS-RMR-Cache to solve Partial-MaxSAT
instances but it is inefficient than Enum-ELS-RMR-Cache to
solve plain MaxSAT instances.