Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper investigates the complexity and implementation of 2-ASP(Q)^w programs, a fragment of Answer Set Programming with Quantifiers capable of expressing optimization problems up to Delta_3^P. The authors provide a complete complexity characterization of key computational tasks for this class of programs. They also introduce and evaluate novel Counterexample-Guided Abstraction Refinement (CEGAR) techniques within the Casper system for computing quantified answer sets, demonstrating practical effectiveness on challenging benchmarks.
Even with quantifiers, Answer Set Programming can be efficiently implemented for complex optimization problems using Counterexample-Guided Abstraction Refinement.
ASP(Q) extends Answer Set Programming (ASP) with Quantifiers over answer sets. In this paper we focus on the class of ASP(Q) programs with two quantifiers and weak constraints, denoted as 2-ASP(Q)^w. 2-ASP(Q)^w is a practically relevant fragment of ASP(Q) that is expressive enough to capture optimization problems up to the class Delta_3^P. On the theoretical side, we provide a complete complexity characterization of the main computational tasks for 2-ASP(Q)^w programs, including tight completeness results and the analysis of nontrivial cases that have not been addressed in previous works. On the practical side, we introduce novel strategies for computing (optimal) quantified answer sets in the Casper system, that rely on a Counterexample-Guided Abstraction Refinement (CEGAR) technique tailored to ASP(Q). An experimental evaluation on hard benchmarks from different application domains shows that the proposed techniques are effective in practice.