The ASP(Q) language extends Answer Set Programming (ASP) with Quantifiers that operate over answer sets. Thus, ASP(Q) facilitates a more natural encoding of problems whose complexity exceeds NP within the ASP framework. 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 Polynomial Hierarchy. 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 state-of-the-art ASP(Q) solvers, across benchmark problems located at the second level of the polynomial hierarchy.

Linear Temporal Logic over finite traces (LTLf) is a widely used formalism with applications in AI, process mining, model checking, and more. The primary reasoning task for LTLf is satisfiability checking; yet, the recent focus on explainable AI has increased interest in analyzing inconsistent formulae, making the enumeration of minimal explanations for unsatisfiability a relevant task also for LTLf. We introduce a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an LTLf specification. The main idea is to encode an LTLf formula into an Answer Set Programming (ASP) specification, such that the minimal unsatisfiable subsets (MUSes) of the ASP program directly correspond to the MUCs of the original LTLf specification. Leveraging recent advancements in ASP solving yields an MUC enumerator achieving good performance in experiments conducted on established benchmarks from the literature.

Answer Set Programming with Quantifiers (ASP(Q)) extends Answer Set Programming (ASP) by allowing quantification over answer sets. Although probabilistic extensions to ASP exist, there is no such counterpart for ASP(Q). In this paper, we close this gap by introducing Inferential Quantified Answer Set Programming (ASP(Q)Inf), an extension of ASP(Q) that supports probabilistic inference over programs with alternating quantifiers, allowing uncertainty at the innermost level. We demonstrate the modeling capabilities of ASP(Q)Inf, analyze its computational complexity, and present an implementation based on Algebraic Model Counting. An experimental evaluation confirms its effectiveness and practical applicability.

We explore the use of answer set programming (ASP) and its extension with quantifiers, ASP(Q), for inconsistency-tolerant querying of prioritized data, where a priority relation between conflicting facts is exploited to define three notions of optimal repairs (Pareto-, globally- and completion-optimal). We consider the variants of three well-known semantics (AR, brave and IAR) that use these optimal repairs, and for which query answering is in the first or second level of the polynomial hierarchy for a large class of logical theories. Notably, this paper presents the first implementation of globally-optimal repair-based semantics, as well as the first implementation of the grounded semantics, which is a tractable under-approximation of all these optimal repair-based semantics. Our experimental evaluation sheds light on the feasibility of computing answers under globally-optimal repair semantics and the impact of adopting different semantics, approximations, and encodings.

Maximum-a-Posteriori (MAP) inference is a crucial problem in Artificial Intelligence, which requires both marginalization and maximization, and asks for the most probable value for a given set of variables such that an evidence holds. Several languages within the Statistical Relational Artificial Intelligence landscape support the encoding of MAP. Here, we focus on Probabilistic Answer Set Programming, consider the credal and smProbLog semantics, and introduce a three-level algebraic model counting representation for MAP. We implemented our approach on top of a state-of-the-art solver and compared it with existing solutions, showing the competitive performance of our proposal, even against less general tools.

Most Probable Explanation (MPE) is a fundamental problem in statistical relational artificial intelligence. In the context of Probabilistic Answer Set Programming (PASP), solving MPE is still an open research problem. In this paper, we present three novel approaches for solving the MPE task in PASP that are based on: i) Algebraic Model Counting, ii) Answer Set Programming (ASP), and iii) ASP with quantifiers (ASP(Q)). These approaches are implemented and evaluated against existing solvers across different datasets and configurations. Empirical results demonstrate that the novel solutions consistently outperform existing alternatives for non-stratified programs.

Probabilistic logic-based languages offer an expressive framework for encoding uncertain information in a human-interpretable way. Among existing formalisms, Probabilistic Answer Set Programming (PASP) stands out for its ease of modeling complex scenarios. The current definition of PASP is limited to programs consisting of disjunctive rules and probabilistic facts only. To enhance the expressivity of the framework, we introduce Optimal Probabilistic Answer Set Programming, which extends the language by allowing the inclusion of weak constraints within PASP specifications. We motivate this extension through some real-world application scenarios and present a detailed computational complexity analysis for both the inference and Most Probable Explanation (MPE) tasks.

Answer Set Programming (ASP) is a widely recognized formalism for Knowledge Representation and Reasoning. Traditional ASP systems, that employ the ground and solve architecture, are subject to the grounding bottleneck (i.e., variable-elimination can exhaust all computational resources). Compilation-based approaches have recently demonstrated how grounding can be effectively bypassed by compiling rules into propagators that simulate them. However, compiling an entire ASP program is not always advantageous. In this paper, we present both a program rewriting technique and an algorithm for the compilation of grounding that allow for unrestricted blending of grounding and compilation. We implement these techniques in a hybrid ASP system that compares favourably with state-of-the-art ASP solvers on established benchmarks.

Abstract Unit testing frameworks are nowadays considered a best practice, included in almost all modern software development processes, to achieve rapid development of correct specifications. Knowledge representation and reasoning paradigms such as Answer Set Programming (ASP), that have been used in industry-level applications, are not an exception. Indeed, the first unit testing specification language for ASP was proposed in 2011 as a feature of the ASPIDE development environment. Later, a more portable unit testing language was included in the LANA annotation language. In this paper we revisit both languages and tools for unit testing in ASP. We propose a new unit test specification language that allows one to inline tests within ASP programs, and we identify the computational complexity of the tasks associated with checking the various program-correctness assertions. Test-case specifications are transparent to the traditional evaluation, but can be interpreted by a specific testing tool. Thus, we present a novel environment supporting test-driven development of ASP programs.

Abstract Answer Set Programming with Quantifiers (ASP(Q)) has been introduced to provide a natural extension of ASP modeling to problems in the polynomial hierarchy (PH). However, ASP(Q) lacks a method for encoding in an elegant and compact way problems requiring a polynomial number of calls to an oracle in $\Sigma _n^p$ (that is, problems in $\Delta _{n+1}^p$ ). Such problems include, in particular, optimization problems. In this paper, we propose an extension of ASP(Q), in which component programs may contain weak constraints. Weak constraints can be used both for expressing local optimization within quantified component programs and for modeling global optimization criteria. We showcase the modeling capabilities of the new formalism through various application scenarios. Further, we study its computational properties obtaining complexity results and unveiling non-obvious characteristics of ASP(Q) programs with weak constraints.

Answer Set Programming (ASP) is a well-known AI formalism. Traditional ASP systems, that follow the “ground&solve” approach, are intrinsically limited by the so-called grounding bottleneck. Basically, the grounding step (i.e., variable-elimination) can be computationally expensive, and even unfeasible in several cases of practical interest. Recent work demonstrated that the grounding bottleneck can be partially overcome by compiling in external propagators subprograms acting as constraints. In this paper a novel compilation technique is presented that can be applied to tight normal programs; thus, the class of ASP programs that can be compiled is extended beyond constraints. The approach is implemented in the new system PROASP. PROASP skips entirely the grounding phase and performs solving by injecting custom propagators in GLUCOSE. An experiment, conducted on grounding-intensive ASP benchmarks, shows that PROASP is capable of solving instances that are out of reach for state-of-the-art ASP systems.

Abstract 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 subclauses. 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.

Answer Set Programming (ASP) is a well-known declarative AI formalism for knowledge representation and reasoning. State-of-the-art ASP implementations employ the ground&solve approach, and they were successfully applied to industrial and academic problems. Nonetheless there are classes of ASP programs whose evaluation is not efficient (sometimes not feasible) due to the combinatorial blow-up of the program produced by the grounding step. Recent researches suggest that compilation-based techniques can mitigate the grounding bottleneck problem. However, no compilation-based technique has been developed for ASP programs that contain aggregates, which are one of the most relevant and commonly-employed constructs of ASP. In this paper, we propose a compilation-based approach for ASP programs with aggregates. We implement it on top of a state-of-the-art ASP system, and evaluate the performance on publicly-available benchmarks. Experiments show our approach is effective on ground-intensive ASP programs.