Cautious reasoning in ASP via minimal models and unsatisfiable cores

TL;DR

This paper introduces new algorithms for cautious reasoning in ASP that leverage minimal models and unsatisfiable cores, improving efficiency over existing methods in computing cautious consequences.

Contribution

It proposes novel algorithms for cautious reasoning in ASP using minimal models and unsatisfiable cores, enhancing solver performance.

Findings

New algorithms outperform state-of-the-art in benchmarks

Implementation in WASP shows improved efficiency

Algorithms effectively discard more candidates during search

Abstract

Answer Set Programming (ASP) is a logic-based knowledge representation framework, supporting---among other reasoning modes---the central task of query answering. In the propositional case, query answering amounts to computing cautious consequences of the input program among the atoms in a given set of candidates, where a cautious consequence is an atom belonging to all stable models. Currently, the most efficient algorithms either iteratively verify the existence of a stable model of the input program extended with the complement of one candidate, where the candidate is heuristically selected, or introduce a clause enforcing the falsity of at least one candidate, so that the solver is free to choose which candidate to falsify at any time during the computation of a stable model. This paper introduces new algorithms for the computation of cautious consequences, with the aim of driving the solver to search for stable models discarding more candidates. Specifically, one of such algorithms enforces minimality on the set of true candidates, where different notions of minimality can be used, and another takes advantage of unsatisfiable cores computation. The algorithms are implemented in WASP, and experiments on benchmarks from the latest ASP competitions show that the new algorithms perform better than the state of the art. (Under consideration for acceptance in TPLP).