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

Okamoto, Keishi, Kido, Hiroyuki, Takai, Toshinori

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.

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

Search this article

Description

Journal

Details 詳細情報について

Export

Report a problem