# An efficient solver for ASP(Q)

arXiv: https://arxiv.org/abs/2305.10021 · HTML: https://mlsanity.com/paper/2305.10021/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 28 references that are in the map.
- First posted on arXiv 17 May 2023.

## Builds on (most cited first, 6 of 6)

- [Planning with Incomplete Information in Quantified Answer Set Programming](https://mlsanity.com/paper/2108.06405/) (2021)
- [A Multi-Engine Approach to Answer Set Programming](https://mlsanity.com/paper/1306.4925/) (2013)
- [Beyond NP: Quantifying over Answer Sets](https://mlsanity.com/paper/1907.09559/) (2019)
- [Stable-Unstable Semantics: Beyond NP with Normal Logic Programs](https://mlsanity.com/paper/1608.01835/) (2016)
- [Efficiently Coupling the I-DLV Grounder with ASP Solvers](https://mlsanity.com/paper/1810.00041/) (2018)
- [New Models for Generating Hard Random Boolean Formulas and Disjunctive Logic Programs](https://mlsanity.com/paper/1802.03828/) (2018)

## Built on by (most cited first, 2 of 2)

- [Using ASP(Q) to Handle Inconsistent Prioritized Data](https://mlsanity.com/paper/2604.21603/) (2026)
- [2-ASP(Q) programs with weak constraints: Complexity and efficient implementation](https://mlsanity.com/paper/2605.27338/) (2026)

## Abstract (arXiv)

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.