2-ASP(Q) Programs with Weak Constraints: Complexity and Efficient Implementation

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 Superscript w w ʷ (Q). 2-ASP Superscript w w ʷ (Q) is a practically relevant fragment of ASP(Q) that is expressive enough to capture optimization problems up to the class normal upper Delta 3 Superscript upper P Δ 3 P Δ P₃ . On the theoretical side, we provide a complete complexity characterization of the main computational tasks for 2-ASP Superscript w w ʷ (Q) 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.