Answer Set Programming with Quantifiers ASP(Q) extends Answer Set Programming (ASP) to allow for declarative and modular modeling of problems from the entire polynomial hierarchy. The first implementation of ASP(Q), called qasp, was based on a translation to Quantified Boolean Formulae (QBF) with the aim of exploiting the well-developed and mature QBF-solving technology. However, the implementation of the QBF encoding employed in qasp is very general and might produce formulas that are hard to evaluate for existing QBF solvers because of the large number of symbols and sub-clauses. In this paper, we present a new implementation that builds on the ideas of qasp and features both a more efficient encoding procedure and new optimized encodings of ASP(Q) programs in QBF. The new encodings produce smaller formulas (in terms of the number of quantifiers, variables, and clauses) and result in a more efficient evaluation process. An algorithm selection strategy automatically combines several QBF-solving back-ends to further increase performance. An experimental analysis, conducted on known benchmarks, shows that the new system outperforms qasp.

翻译：带量词的回答集编程ASP(Q)扩展了回答集编程（ASP），允许对来自整个多项式层次的问题进行声明式和模块化建模。ASP(Q)的第一个实现称为qasp，基于到量化布尔公式（QBF）的翻译，旨在利用成熟且发达的QBF求解技术。然而，qasp中采用的QBF编码实现非常通用，可能因大量符号和子句而产生现有QBF求解器难以评估的公式。本文提出了一种新实现，它建立在qasp思想的基础上，具有更高效的编码过程以及针对ASP(Q)程序的新优化QBF编码。新编码生成更小的公式（从量词、变量和子句数量角度而言），并实现更高效的评估过程。一种算法选择策略自动组合多个QBF求解后端以进一步提高性能。在已知基准上进行的实验分析表明，新系统优于qasp。