Special-purpose propagators speed up solving logic programs by inferring facts that are hard to deduce otherwise. However, implementing special-purpose propagators is a non-trivial task and requires expert knowledge of solvers. This paper proposes a novel approach in logic programming that allows (1) logical specification of both the problem itself and its propagators and (2) automatic incorporation of such propagators into the solving process. We call our proposed language P[R] and our solver SAT-to-SAT because it facilitates communication between several SAT solvers. Using our proposal, non-specialists can specify new reasoning methods (propagators) in a declarative fashion and obtain a solver that benefits from both state-of-the-art techniques implemented in SAT solvers as well as problem-specific reasoning methods that depend on the problem's structure. We implement our proposal and show that it outperforms the existing approach that only allows modeling a problem but does not allow modeling the reasoning methods for that problem.

Abstract Standard answer set programming (ASP) targets at solving search problems from the first level of the polynomial time hierarchy (PH). Tackling search problems beyond NP using ASP is less straightforward. The class of disjunctive logic programs offers the most prominent way of reaching the second level of the PH, but encoding respective hard problems as disjunctive programs typically requires sophisticated techniques such as saturation or meta-interpretation. The application of such techniques easily leads to encodings that are inaccessible to non-experts. Furthermore, while disjunctive ASP solvers often rely on calls to a (co-)NP oracle, it may be difficult to detect from the input program where the oracle is being accessed. In other formalisms, such as Quantified Boolean Formulas (QBFs), the interface to the underlying oracle is more transparent as it is explicitly recorded in the quantifier prefix of a formula. On the other hand, ASP has advantages over QBFs from the modeling perspective. The rich high-level languages such as ASP-Core-2 offer a wide variety of primitives that enable concise and natural encodings of search problems. In this paper, we present a novel logic programming–based modeling paradigm that combines the best features of ASP and QBFs. We develop so-calledcombined logic programsin which oracles are directly cast as (normal) logic programs themselves. Recursive incarnations of this construction enable logic programming on arbitrarily high levels of the PH. We develop a proof-of-concept implementation for our new paradigm.