2-ASP(Q) Solving Based on CEGAR

The ASP(Q) language extends Answer Set Programming (ASP) with Quantifiers that operate over answer sets. In this way, ASP(Q) allows for natural modeling of problems of complexity beyond NP with ASP. In this paper we focus on ASP(Q) programs with two quantifiers, i.e., 2-ASP(Q) programs, which can be used to model problems in the second level of the PH. In particular, we propose an approach for evaluating 2-ASP(Q) programs that is inspired by Counterexample Guided Abstraction Refinement (CEGAR). Unlike existing state-of-the-art ASP(Q) solvers, which are typically based on QBF solvers, our new approach leverages ASP solvers, and suffers no overhead due to the effects of translating ASP(Q) in QBF. Experimental results demonstrate that our technique consistently outperforms both state-of-the-art ASP(Q) solvers and ASP solvers that rely on disjunctive encodings, across benchmark problems located at the second level of the polynomial hierarchy.