Armando Tacchella

IROS Conference 2025 Conference Paper

Code Generation and Monitoring for Deliberation Components in Autonomous Robots

• Stefano Bernagozzi
• S. Faraci
• Enrico Ghiorzi
• K. Pedemonte
• Lorenzo Natale
• Armando Tacchella

Hand-coded deliberation components are prone to flaws that may not be discovered before deployment and that can be harmful to the robot and its execution environment, including the people within it. To reduce development effort and at the same time increase confidence in robot’s safety, we propose to model deliberation components at a conceptual level, to automatically generate code from such models and also to monitor their execution during robot operation. We present two tools, one which compiles models of deliberation components into executable code, and one which generates runtime monitors from the models. We have tested them in simulation, to demonstrate the usefulness of combining together model-based development, code generation, and monitoring.

JELIA Conference 2023 Conference Paper

Optimal Planning with Expressive Action Languages as Constraint Optimization

• Enrico Giunchiglia
• Armando Tacchella

Abstract We consider the problem of optimal planning in deterministic domains specified with expressive action languages. We show how it is possible to reduce such problem to finding an optimal solution of a constraint optimization problem incorporating a bound n on the maximum length of the plan. By solving the latter, we can conclude whether ( i ) the plan found is optimal even for bounds greater than n; or ( ii ) we need to increase n; or ( iii ) it is useless to increase n since the planning problem has no solution.

IROS Conference 2021 Conference Paper

Formalizing the Execution Context of Behavior Trees for Runtime Verification of Deliberative Policies

• Michele Colledanchise
• Giuseppe Cicala
• Daniele E. Domenichelli
• Lorenzo Natale
• Armando Tacchella

In this paper, we enable automated property verification of deliberative components in robot control architectures. We focus on formalizing the execution context of Behavior Trees (BTs) to provide a scalable, yet formally grounded, methodology to enable runtime verification and prevent unexpected robot behaviors. To this end, we consider a message-passing model that accommodates both synchronous and asynchronous composition of parallel components, in which BTs and other components execute and interact according to the communication patterns commonly adopted in robotic software architectures. We introduce a formal property specification language to encode requirements and build runtime monitors. We performed a set of experiments, both on simulations and on the real robot, demonstrating the feasibility of our approach in a realistic application and its integration in a typical robot software architecture. We also provide an OS-level virtualization environment to reproduce the experiments in the simulated scenario.

IJCAI Conference 2020 Conference Paper

Optimal Planning Modulo Theories

• Francesco Leofante
• Enrico Giunchiglia
• Erika Ábráham
• Armando Tacchella

We consider the problem of planning with arithmetic theories, and focus on generating optimal plans for numeric domains with constant and state-dependent action costs. Solving these problems efficiently requires a seamless integration between propositional and numeric reasoning. We propose a novel approach that leverages Optimization Modulo Theories (OMT) solvers to implement a domain-independent optimal theory-planner. We present a new encoding for optimal planning in this setting and we evaluate our approach using well-known, as well as new, numeric benchmarks.

ECAI Conference 2020 Conference Paper

Verification of Neural Networks: Enhancing Scalability Through Pruning

• Dario Guidotti
• Francesco Leofante
• Luca Pulina
• Armando Tacchella

Verification of deep neural networks has witnessed a recent surge of interest, fueled by success stories in diverse domains and by abreast concerns about safety and security in envisaged applications. Complexity and sheer size of such networks are challenging for automated formal verification techniques which, on the other hand, could ease the adoption of deep networks in safety- and security-critical contexts. In this paper we focus on enabling state-of-the-art verification tools to deal with neural networks of some practical interest. We propose a new training pipeline based on network pruning with the goal of striking a balance between maintaining accuracy and robustness, while also making the resulting networks amenable to formal analysis. The results of our experiments with a portfolio of pruning algorithms and verification tools show that our approach is successful for the kind of networks we consider and for some combinations of pruning and verification techniques, thus bringing deep neural networks closer to the reach of formally-grounded methods.

ICAPS Conference 2019 Conference Paper

Cyber-Physical Planning: Deliberation for Hybrid Systems with a Continuous Numeric State

• Arthur Bit-Monnot
• Luca Pulina
• Armando Tacchella

Cyber-physical systems pose unique deliberation challenges, where complex strategies must be autonomously derived and executed in the physical world, relying on continuous state representations and subject to safety and security constraints. Robots are a typical example of cyber-physical systems where high-level decisions must be reconciled with motion-level decisions in order to provide guarantees on the validity and efficiency of the plan. In this work we propose techniques to refine a high-level plan into a continuous state trajectory. The refinement is done by translating a high-level plan into a nonlinear optimization problem with constraints that can encode the intrinsic limitations and dynamics of the system as well as the rules for its continuous control. The refinement process either succeeds or yields an explanation that we exploit to refine the search space of a domain-independent task planner. We evaluate our approach on existing PDDL+ benchmarks and on a more realistic and challenging rover navigation problem.

SAT Conference 2018 Conference Paper

Constrained Image Generation Using Binarized Neural Networks with Decision Procedures

• Svyatoslav Korneev
• Nina Narodytska
• Luca Pulina
• Armando Tacchella
• Nikolaj S. Bjørner
• Shmuel Sagiv

Abstract We consider the problem of binary image generation with given properties. This problem arises in a number of practical applications, including generation of artificial porous medium for an electrode of lithium-ion batteries, for composed materials, etc. A generated image represents a porous medium and, as such, it is subject to two sets of constraints: topological constraints on the structure and process constraints on the physical process over this structure. To perform image generation we need to define a mapping from a porous medium to its physical process parameters. For a given geometry of a porous medium, this mapping can be done by solving a partial differential equation (PDE). However, embedding a PDE solver into the search procedure is computationally expensive. We use a binarized neural network to approximate a PDE solver. This allows us to encode the entire problem as a logical formula. Our main contribution is that, for the first time, we show that this problem can be tackled using decision procedures. Our experiments show that our model is able to produce random constrained images that satisfy both topological and process constraints.

IROS Conference 2013 Conference Paper

Ensuring safety of policies learned by reinforcement: Reaching objects in the presence of obstacles with the iCub

• Shashank Pathak
• Luca Pulina
• Giorgio Metta
• Armando Tacchella

Given a stochastic policy learned by reinforcement, we wish to ensure that it can be deployed on a robot with demonstrably low probability of unsafe behavior. Our case study is about learning to reach target objects positioned close to obstacles, and ensuring a reasonably low collision probability. Learning is carried out in a simulator to avoid physical damage in the trial-and-error phase. Once a policy is learned, we analyze it with probabilistic model checking tools to identify and correct potential unsafe behaviors. The whole process is automated and, in principle, it can be integrated step-by-step with routine task-learning. As our results demonstrate, automated fixing of policies is both feasible and highly effective in bounding the probability of unsafe behaviors.

AAAI Conference 2010 Conference Paper

Collaborative Expert Portfolio Management

• David Stern
• Horst Samulowitz
• Ralf Herbrich
• Thore Graepel
• Luca Pulina
• Armando Tacchella

We consider the task of assigning experts from a portfolio of specialists in order to solve a set of tasks. We apply a Bayesian model which combines collaborative filtering with a feature-based description of tasks and experts to yield a general framework for managing a portfolio of experts. The model learns an embedding of tasks and problems into a latent space in which affinity is measured by the inner product. The model can be trained incrementally and can track non-stationary data, tracking potentially changing expert and task characteristics. The approach allows us to use a principled decision theoretic framework for expert selection, allowing the user to choose a utility function that best suits their objectives. The model component for taking into account the performance feedback data is pluggable, allowing flexibility. We apply the model to manage a portfolio of algorithms to solve hard combinatorial problems. This is a well studied area and we demonstrate a large improvement on the state of the art in one domain (constraint solving) and in a second domain (combinatorial auctions) created a portfolio that performed significantly better than any single algorithm.

ICRA Conference 2010 Conference Paper

Safe and effective learning: A case study

• Giorgio Metta
• Lorenzo Natale
• Shashank Pathak
• Luca Pulina
• Armando Tacchella

In this paper we consider the problem of ensuring that a multi-agent robot control system is both safe and effective in the presence of learning components. Safety, i. e. , proving that a potentially dangerous configuration is never reached in the control system, usually competes with effectiveness, i. e. , ensuring that tasks are performed at an acceptable level of quality. In particular, we focus on a robot playing the air hockey game against a human opponent, where the robot has to learn how to minimize opponent's goals (defense play). This setup is paradigmatic since the robot must see, decide and move fastly, but, at the same time, it must learn and guarantee that the control system is safe throughout the process. We attack this problem using automata-theoretic formalisms and associated verification tools, showing experimentally that our approach can yield safety without heavily compromising effectiveness.

SAT Conference 2010 Conference Paper

The Seventh QBF Solvers Evaluation (QBFEVAL'10)

• Claudia Peschiera
• Luca Pulina
• Armando Tacchella
• Uwe Bubeck
• Oliver Kullmann
• Inês Lynce

Abstract In this paper we report about QBFEVAL’10, the seventh in a series of events established with the aim of assessing the advancements in reasoning about quantified Boolean formulas (QBFs). The paper discusses the results obtained and the experimental setup, from the criteria used to select QBF instances to the evaluation infrastructure. We also discuss the current state-of-the-art in light of past challenges and we envision future research directions that are motivated by the results of QBFEVAL’10.

IJCAI Conference 2009 Conference Paper

• Luca Pulina
• Armando Tacchella

In this paper we approach the problem of reasoning with quantified Boolean formulas (QBFs) by combining search and resolution, and by switching between them according to structural properties of QBFs. We provide empirical evidence that QBFs which cannot be solved by search or resolution alone, can be solved by combining them, and that our approach makes a proof-of-concept implementation competitive with current QBF solvers.

LPAR Conference 2008 Conference Paper

Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings

• Luca Pulina
• Armando Tacchella

Abstract Theoretical studies show that in some combinatorial problems, there is a close relationship between classes of tractable instances and the treewidth ( tw ) of graphs describing their structure. In the case of satisfiability for quantified Boolean formulas (QBFs), tractable classes can be related to a generalization of treewidth, that we call quantified treewidth ( tw p ). In this paper we investigate the practical relevance of computing tw p for problem domains encoded as QBFs. We show that an approximation of tw p is a predictor of empirical hardness, and that it is the only parameter among several other candidates which succeeds consistently in being so. We also provide evidence that QBF solvers benefit from a preprocessing phase geared towards reducing tw p, and that such phase is a potential enabler for the solution of hard QBF encodings.

JELIA Conference 2006 Conference Paper

The QBFEVAL Web Portal

• Massimo Narizzano
• Luca Pulina
• Armando Tacchella

Abstract In this paper we describe the QBFEVAL web portal, an on-line resource supporting the participants and the organizers of the yearly evaluation of QBF solvers and instances.

SAT Conference 2004 Conference Paper

QBF Reasoning on Real-World Instances

• Enrico Giunchiglia
• Massimo Narizzano
• Armando Tacchella

During the recent years, the development of tools for deciding Quantified Boolean Formulas (QBFs) has been accompanied by a steady supply of real-world instances, i.e., QBFs originated by translations from application domains. Instances of this kind showed to be challenging for current state-of-the-art QBF solvers, while the ability to deal effectively with them is necessary to foster adoption of QBF-based reasoning in practice. In this paper we describe three reasoning techniques that we implemented in our solver Q U BE++ to increase its performances on real-world instances coming from formal verification and planning domains. We present experimental results that witness the contribution of each technique and the better performances of Q U BE++ with respect to other state-of-the-art QBF solvers. The effectiveness of Q U BE++ is further confirmed by experiments run on challenging real-world SAT instances, where Q U BE++ turns out to be competitive with respect to current state-ofthe-art SAT solvers.

AIJ Journal 2003 Journal Article

Backjumping for Quantified Boolean Logic satisfiability

• Enrico Giunchiglia
• Massimo Narizzano
• Armando Tacchella

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision procedures have been proposed in the last few years, most of them based on the Davis, Logemann, Loveland procedure (DLL) for propositional satisfiability (SAT). In this paper we show how it is possible to extend the conflict-directed backjumping schema for SAT to the satisfiability of QBFs: When applicable, conflict-directed backjumping allows search to skip over existentially quantified literals while backtracking. We introduce solution-directed backjumping, which allows the same behavior for universally quantified literals. We show how it is possible to incorporate both conflict-directed and solution-directed backjumping in a DLL-based decision procedure for satisfiability of QBFs. We also implement and test the procedure: The experimental analysis shows that, because of backjumping, significant speed-ups can be obtained. Summing up: We present the first algorithm that applies conflict and solution directed backjumping to QBF, and demonstrate the performance of this algorithm via an empirical study.

SAT Conference 2003 Conference Paper

Challenges in the QBF Arena: the SAT'03 Evaluation of QBF Solvers

• Daniel Le Berre
• Laurent Simon 0001
• Armando Tacchella

Abstract The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important issue in several research fields such as Formal Verification, Planning, and Reasoning about Knowledge. Several QBF solvers have been implemented in the last few years, most of them extending the well-known Davis, Putnam, Logemann, Loveland procedure (DPLL) for propositional satisfiability (SAT). At the same time, a substantial breed of QBF benchmarks emerged, both in the form of statistical models for the generation of random formulas, and in the form of real-world instances. In this paper we report about the – first ever – evaluation of QBF solvers that was run as a joint event to SAT’03 Conference on Theory and Applications of Satisfiability Testing. Owing to the relative youngness of QBF tools and applications, we decided to run the comparison on a non-competitive basis, using the same technology that powered SAT’02 and SAT’03 competitions of SAT solvers. Running the evaluation enabled us to collect all sorts of data regarding the relative strength of different solvers and methods, the quality of the benchmarks, and to understand some of the current challenges for researchers involved in the QBF arena.

AIJ Journal 2003 Journal Article

SAT-based planning in complex domains: Concurrency, constraints and nondeterminism

• Claudio Castellini
• Enrico Giunchiglia
• Armando Tacchella

Planning as satisfiability is a very efficient technique for classical planning, i. e. , for planning domains in which both the effects of actions and the initial state are completely specified. In this paper we present C -sat, a SAT-based procedure capable of dealing with planning domains having incomplete information about the initial state, and whose underlying transition system is specified using the highly expressive action language C. Thus, C -sat allows for planning in domains involving (i) actions which can be executed concurrently; (ii) (ramification and qualification) constraints affecting the effects of actions; and (iii) nondeterminism in the initial state and in the effects of actions. We first prove the correctness and the completeness of C -sat, discuss some optimizations, and then we present C -plan, a system based on C -sat. C -plan works on any C planning problem, but some optimizations have not been fully implemented yet. Nevertheless, the experimental analysis shows that SAT-based approaches to planning with incomplete information are viable, at least in the case of problems with a high degree of parallelism.

SAT Conference 2003 Conference Paper

Watched Data Structures for QBF Solvers

• Ian P. Gent
• Enrico Giunchiglia
• Massimo Narizzano
• Andrew G. D. Rowley
• Armando Tacchella

Abstract In the last few years, we have seen a tremendous boost in the efficiency of SAT solvers, this boost being mostly due to Chaff. Chaff owes some of its efficiency to its “two-literal watching” data structure. In this paper we present watched data structures for Quantified Boolean Formula (QBF) satisfiability solvers. In particular, we propose ( i ) two Chaff -like literal watching schemes for unit clause detection; and ( ii ) two other watched data structures, one for detecting pure literals and the other for detecting void quantifiers. We have conducted an experimental evaluation of the proposed data structures, using both randomly generated and real-world benchmarks. Our results indicate that clause watching is very effective, while the 2 and 3 literal watching data structures become more effective as the clause length increases. The quantifier watching structure does not appear to be effective on the instances considered.

JELIA Conference 2002 Conference Paper

Dependent and Independent Variables in Propositional Satisfiability

• Enrico Giunchiglia
• Marco Maratea
• Armando Tacchella

Abstract Propositional reasoning (SAT) is central in many applications of Computer Science. Several decision procedures for SAT have been proposed, along with optimizations and heuristics to speed them up. Currently, the most effective implementations are based on the Davis, Logemann, Loveland method. In this method, the input formula is represented as a set of clauses, and the space of truth assignments is searched by iteratively assigning a literal until all the clauses are satisfied, or a clause is violated and backtracking occurs. Once a new literal is assigned, pruning techniques (e. g. , unit propagation) are used to cut the search space by inferring truth values for other variables. In this paper, we investigate the “independent variable selection (IVS) heuristic”, i. e. , given a formula on the set of variables N, the selection is restricted to a - possibly small - subset S which is suficient to determine a truth value for all the variables in N. During the search phase, scoring and selection of the literal to assign next are restricted to S, and the truth values for the remaining variables are determined by the pruning techniques of the solver. We discuss the possible advantages and disadvantages of the IVS heuristic. Our experimental analysis shows that obtaining either positive or negative results strictly depends on the type of problems considered, on the underlying scoring and selection technique, and also on the backtracking scheme.