Expressing Dung's Extensions as FO-Formulas to Enumerate Them with an SMT Solver (Model theoretic aspects of the notion of independence and dimension)

Abstract

It is useful to express constraints for Dung's extensions as FO-formulas so that we can enumerate extensions with an SMT solver. We can extract an extension with a naive SMT solver if we naively express constraints for extensions as FO-formulas. But the definitions of some extensions require maximality /minimality conditions that can not be expressed as FO-formulas. On the other hand, a naive expression is readable but sometimes hard to solve with an SMT solver. Moreover, we need to improve a naive SMT solver to enumerate extensions since an enumeration is an iteration of an extraction. In this paper, we propose a method to enumerate Dung's extensions by solving a Partial Maximal Satisfiable Subsets Enumeration problem, which is an extension of a Maximal Satisfiable Subsets Enumeration problem[l]. In particular, we express hard constraints and soft constraints, which are required for a Partial Maximal Satisfiable Subsets Enumeration problem, with FO-formulas.