Title: Model enumeration in propositional circumscription via unsatisfiable core analysis,
Abstract: Many practical problems are characterized by a preference relation over
admissible solutions, where preferred solutions are minimal in some sense. For
example, a preferred diagnosis usually comprises a minimal set of reasons that
is sufficient to cause the observed anomaly. Alternatively, a minimal
correction subset comprises a minimal set of reasons whose deletion is
sufficient to eliminate the observed anomaly. Circumscription formalizes such
preference relations by associating propositional theories with minimal models.
The resulting enumeration problem is addressed here by means of a new algorithm
taking advantage of unsatisfiable core analysis. Empirical evidence of the
efficiency of the algorithm is given by comparing the performance of the
resulting solver, CIRCUMSCRIPTINO, with HCLASP, CAMUS MCS, LBX and MCSLS on the
enumeration of minimal models for problems originating from practical
applications.
This paper is under consideration for acceptance in TPLP.