Anytime answer set optimization via unsatisfiable core shrinking

TL;DR

This paper introduces an anytime algorithm for answer set optimization that uses unsatisfiable core shrinking, enabling the discovery of suboptimal stable models during the core analysis process, thus improving efficiency.

Contribution

It proposes a novel progression-based shrinking method for unsatisfiable cores, allowing for the computation of suboptimal stable models during core analysis.

Findings

Empirically improves solved instance count

Enables anytime answer set optimization

Finds suboptimal models during core shrinking

Abstract

Unsatisfiable core analysis can boost the computation of optimum stable models for logic programs with weak constraints. However, current solvers employing unsatisfiable core analysis either run to completion, or provide no suboptimal stable models but the one resulting from the preliminary disjoint cores analysis. This drawback is circumvented here by introducing a progression based shrinking of the analyzed unsatisfiable cores. In fact, suboptimal stable models are possibly found while shrinking unsatisfiable cores, hence resulting into an anytime algorithm. Moreover, as confirmed empirically, unsatisfiable core analysis also benefits from the shrinking process in terms of solved instances. This paper is under consideration for acceptance in TPLP.