Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search

Issue title: Special issue devoted to the best paper presented at the 32nd Italian Conference on Computational Logic (CILC 2017)

Guest editors: Dario Della Monica, Aniello Murano and Luigi Sauro

Article type: Research Article

Authors: Alviano, Mario^{a; *} | Dodaro, Carmine^b

Affiliations: [a] Department of Mathematics and Computer Science, University of Calabria, Arcavacata di Rende, Italy. alviano@mat.unical.it | [b] Department of Informatics, Bioengineering, Robotics and Systems Engineering, University of Genova, Genova, Italy. carminedodaro@gmail.com

Correspondence: [*] Address for correspondence: Via Pietro Bucci 30/B, 87036 Rende (CS), Italy

Abstract: Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.

Keywords: Answer Set Programming, weak constraints, unsatisfiable core analysis

DOI: 10.3233/FI-2020-1974

Journal: Fundamenta Informaticae, vol. 176, no. 3-4, pp. 271-297, 2020