Carmine Dodaro

IJCAI Conference 2025 Conference Paper

A General Framework for Representing Controlled Natural Language Sentences and Translation to KR Formalisms

• Simone Caruso
• Carmine Dodaro
• Marco Maratea
• Alice Tarzariol

Languages for Knowledge Representation and Reasoning, such as ASP, CP, and SMT, excel at solving some complex problems, but encoding them into a higher-level language may be more profitable, leaving these formalisms as targets for solving. Recent studies aim to convert controlled natural languages into formal representations, yet these solutions are often tailored to specific languages and require significant effort. This paper introduces a general framework that generates grammars for target representation languages, enabling the translation of problems stated in CNL into formal representations. The related system, CNLWizard, offers a flexible, high-level approach to defining desired grammars, significantly reducing the time and effort needed to create custom grammars. Finally, we demonstrate the system's effectiveness through an experimental analysis.

KR Conference 2025 System Paper

Model Checker for Recursive Aggregates

• Mario Alviano
• Carmine Dodaro
• Salvatore Fiorentino

Model checking for disjunctive logic programs is a co-NP-complete task for which two main state-of-the-art approaches exist: one based on the unsatisfiability of SAT formulas derived from program reducts, and another based on unfounded sets. Although both are effective and efficient, their original formulations do not support recursive aggregates. This paper extends previous work by tackling the stability check problem in the presence of such aggregates. We generalize the reduct-based approach to operate over pseudo-Boolean theories rather than SAT encodings, yielding more compact and efficient formulations. In parallel, we extend the unfounded-set-based approach to incorporate aggregates, integrating both strategies as propagators within the ASP solver clingo. Additionally, we introduce partial stability checks to enable incremental or approximate verification of model stability. Our empirical evaluation demonstrates that these novel strategies not only preserve correctness but also substantially improve the efficiency of model checking for disjunctive programs with aggregates.

IJCAI Conference 2024 Conference Paper

AMO-aware Aggregates in Answer Set Programming

• Mario Alviano
• Carmine Dodaro
• Salvatore Fiorentino
• Marco Maratea

Aggregates such as sum and count are among the most frequently used linguistic extensions of Answer Set Programming (ASP). At-most-one (AMO) constraints are a specific form of aggregates that excludes the simultaneous truth of multiple elements in a set. This article unleashes a powerful propagation strategy in case groups of elements in an aggregate are also involved in AMO constraints. In fact, the combined knowledge given by aggregates and AMO constraints significantly increases the effectiveness of search space pruning, resulting in sensible performance gains.

KR Conference 2024 Conference Paper

Blending Grounding and Compilation for Efficient ASP Solving

• Carmine Dodaro
• Giuseppe Mazzotta
• Francesco Ricca

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.

AIJ Journal 2023 Journal Article

ASP and subset minimality: Enumeration, cautious reasoning and MUSes

• Mario Alviano
• Carmine Dodaro
• Salvatore Fiorentino
• Alessandro Previti
• Francesco Ricca

JELIA Conference 2023 Conference Paper

Comparing Planning Domain Models Using Answer Set Programming

• Lukás Chrpa
• Carmine Dodaro
• Marco Maratea
• Marco Mochi
• Mauro Vallati

Abstract Automated planning is a prominent area of Artificial Intelligence, and an important component for intelligent autonomous agents. A critical aspect of domain-independent planning is the domain model, that encodes a formal representation of domain knowledge needed to reason upon a given problem. Despite the crucial role of domain models in automated planning, there is lack of tools supporting knowledge engineering process by comparing different versions of the models, in particular, determining and highlighting differences the models have. In this paper, we build on the notion of strong equivalence of domain models and formalise a novel concept of similarity of domain models. To measure the similarity of two models, we introduce a directed graph representation of lifted domain models that allows to formulate the domain model similarity problem as a variant of the graph edit distance problem. We propose an Answer Set Programming approach to optimally solve the domain model similarity problem, that identifies the minimum number of modifications the models need to become strongly equivalent, and we demonstrate the capabilities of the approach on a range of benchmark models.

ECAI Conference 2023 Conference Paper

Compilation of Tight ASP Programs

• Carmine Dodaro
• Giuseppe Mazzotta
• Francesco Ricca

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.

AAAI Conference 2022 Conference Paper

Compilation of Aggregates in ASP Systems

• Giuseppe Mazzotta
• Francesco Ricca
• Carmine Dodaro

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 research suggests that compilation-based techniques can mitigate the grounding bottleneck problem. However, no compilationbased 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-theart ASP system, and evaluate the performance on publiclyavailable benchmarks. Experiments show our approach is effective on ground-intensive ASP programs.

IJCAI Conference 2022 Conference Paper

LTL on Weighted Finite Traces: Formal Foundations and Algorithms

• Carmine Dodaro
• Valeria Fionda
• Gianluigi Greco

LTL on finite traces (LTLf ) is a logic that attracted much attention in recent literature, for its ability to formalize the qualitative behavior of dynamical systems in several application domains. However, its practical usage is still rather limited, as LTLf cannot deal with any quantitative aspect, such as with the costs of realizing some desired behaviour. The paper fills the gap by proposing a weighting framework for LTLf encoding such quantitative aspects in the traces over which it is evaluated. The complexity of reasoning problems on weighted traces is analyzed and compared to that of standard LTLf, by considering arbitrary formulas as well as classes of formulas defined in terms of relevant syntactic restrictions. Moreover, a reasoner for LTL on weighted finite traces is presented, and its performances are assessed on benchmark data.

AIJ Journal 2021 Journal Article

Paracoherent answer set computation

• Giovanni Amendola
• Carmine Dodaro
• Wolfgang Faber
• Francesco Ricca

IJCAI Conference 2020 Conference Paper

A Formal Approach for Cautious Reasoning in Answer Set Programming (Extended Abstract)

• Giovanni Amendola
• Carmine Dodaro
• Marco Maratea

The issue of describing in a formal way solving algorithms in various fields such as Propositional Satisfiability (SAT), Quantified SAT, Satisfiability Modulo Theories, Answer Set Programming (ASP), and Constraint ASP, has been relatively recently solved employing abstract solvers. In this paper we deal with cautious reasoning tasks in ASP, and design, implement and test novel abstract solutions, borrowed from backbone computation in SAT. By employing abstract solvers, we also formally show that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. Some of the new solutions have been implemented in the ASP solver WASP, and tested.

IJCAI Conference 2020 Conference Paper

Overcoming the Grounding Bottleneck Due to Constraints in ASP Solving: Constraints Become Propagators

• Bernardo Cuteri
• Carmine Dodaro
• Francesco Ricca
• Peter Schüller

Answer Set Programming (ASP) is a well-known formalism for Knowledge Representation and Reasoning, successfully employed to solve many AI problems, also thanks to the availability of efficient implementations. Traditionally, ASP systems are based on the ground&solve approach, where the grounding transforms a general input program into its propositional counterpart, whose stable models are then computed by the solver using the CDCL algorithm. This approach suffers an intrinsic limitation: the grounding of one or few constraints may be unaffordable from a computational point of view; a problem known as grounding bottleneck. In this paper, we develop an innovative approach for evaluating ASP programs, where some of the constraints of the input program are not grounded but automatically translated into propagators of the CDCL algorithm that work on partial interpretations. We implemented the new approach on top of the solver WASP and carried out an experimental analysis on different benchmarks. Results show that our approach consistently outperforms state-of-the-art ASP systems by overcoming the grounding bottleneck.

JELIA Conference 2019 Conference Paper

Algorithm Selection for Paracoherent Answer Set Computation

• Giovanni Amendola
• Carmine Dodaro
• Wolfgang Faber 0001
• Luca Pulina
• Francesco Ricca

Abstract Answer Set Programming (ASP) is a well-established AI formalism rooted in nonmonotonic reasoning. Paracoherent semantics for ASP have been proposed to derive useful conclusions also in the absence of answer sets caused by cyclic default negation. Recently, several different algorithms have been proposed to implement them, but no algorithm is always preferable to the others in all instances. In this paper, we apply algorithm selection techniques to devise a more efficient paracoherent answer set solver combining existing algorithms. The effectiveness of the approach is demonstrated empirically running our system on existing benchmarks.

KR Conference 2018 Conference Paper

A Hybrid Approach to Optimization in Answer Set Programming

• Paul Saikko
• Carmine Dodaro
• Mario Alviano
• Matti Järvisalo

Answer set programming (ASP) is today a successful approach to knowledge representation and reasoning in various real-world problem domains. ASP offers an expressive rule-based constraint modelling language, supporting concise declarative modelling of both decision and optimization problems within the first or the second level of the polynomial hierarchy. In this paper, we propose a new approach to solving optimization problems via ASP, i. e. , to the problem of finding optimal solutions (in terms of optimal answer sets or stable models) under a given weight function over soft atoms (weak constraints). Our approach constitutes the first adaptation of the so-called implicit hitting set approach in the context of ASP. In particular, in contrast to the earlier proposed family of core-guided algorithms for optimization in answer set programming, we present a hybrid approach which makes use of interactions between an ASP decision solver (as an unsatisfiable core extractor) and an integer programming solver (as a minimum-cost hitting set algorithm). We explain how various concepts and features specific to ASP and IP can be harnessed within the approach, including several ways for obtaining better upper and lower bounds during search, with the aim of speeding up the computation of an optimal answer set. By a careful integration of the interactions between state-of-the-art ASP and IP solvers, we show that already our first implementation provides a complementary approach when empirically compared to the currently available solvers supporting optimization in answer set programming.

AAAI Conference 2018 Conference Paper

Externally Supported Models for Efficient Computation of Paracoherent Answer Sets

• Giovanni Amendola
• Carmine Dodaro
• Wolfgang Faber
• Francesco Ricca

Answer Set Programming (ASP) is a well-established formalism for nonmonotonic reasoning. While incoherence, the non-existence of answer sets for some programs, is an important feature of ASP, it has frequently been criticised and indeed has some disadvantages, especially for query answering. Paracoherent semantics have been suggested as a remedy, which extend the classical notion of answer sets to draw meaningful conclusions also from incoherent programs. In this paper we present an alternative characterization of the two major paracoherent semantics in terms of (extended) externally supported models. This definition uses a transformation of ASP programs that is more parsimonious than the classic epistemic transformation used in recent implementations. A performance comparison carried out on benchmarks from ASP competitions shows that the usage of the new transformation brings about performance improvements that are independent of the underlying algorithms.

AAAI Conference 2017 Conference Paper

On the Computation of Paracoherent Answer Sets

• Giovanni Amendola
• Carmine Dodaro
• Wolfgang Faber
• Nicola Leone
• Francesco Ricca

Answer Set Programming (ASP) is a well-established formalism for nonmonotonic reasoning. An ASP program can have no answer set due to cyclic default negation. In this case, it is not possible to draw any conclusion, even if this is not intended. Recently, several paracoherent semantics have been proposed that address this issue, and several potential applications for these semantics have been identified. However, paracoherent semantics have essentially been inapplicable in practice, due to the lack of efficient algorithms and implementations. In this paper, this lack is addressed, and several different algorithms to compute semi-stable and semi-equilibrium models are proposed and implemented into an answer set solving framework. An empirical performance comparison among the new algorithms on benchmarks from ASP competitions is given as well.

IJCAI Conference 2017 Conference Paper

Unsatisfiable Core Shrinking for Anytime Answer Set Optimization

• Mario Alviano
• Carmine Dodaro

Efficient algorithms for the computation of optimum stable models are based on unsatisfiable core analysis. However, these algorithms essentially run to completion, providing few or even no suboptimal stable models. This drawback can be circumvented by shrinking unsatisfiable cores. Interestingly, the resulting anytime algorithm can solve more instances than the original algorithm.

IJCAI Conference 2016 Conference Paper

Completion of Disjunctive Logic Programs

• Mario Alviano
• Carmine Dodaro

Clark's completion plays an important role in ASP computation: it discards unsupported models via unit resolution; hence, it improves the performance of ASP solvers, and at the same time it simplifies their implementation. In the disjunctive case, however, Clark's completion is usually preceded by another transformation known as shift, whose size is quadratic in general. A different approach is proposed in this paper: Clark's completion is extended to disjunctive programs without the need of intermediate program rewritings such as the shift. As in the non-disjunctive case, the new completion is linear in size, and discards unsupported models via unit resolution. Moreover, an ad-hoc propagator for supported model search is presented.

IJCAI Conference 2015 Conference Paper

A MaxSAT Algorithm Using Cardinality Constraints of Bounded Size

• Mario Alviano
• Carmine Dodaro
• Francesco Ricca

Core-guided algorithms proved to be effective on industrial instances of MaxSAT, the optimization variant of the satisfiability problem for propositional formulas. These algorithms work by iteratively checking satisfiability of a formula that is relaxed at each step by using the information provided by unsatisfiable cores. The paper introduces a new core-guided algorithm that adds cardinality constraints for each detected core, but also limits the number of literals in each constraint in order to control the number of refutations in subsequent satisfiability checks. The performance gain of the new algorithm is assessed on the industrial instances of the 2014 MaxSAT Evaluation.