Author name cluster

Roberto Sebastiani

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

25 papers

2 author rows

UAI Conference 2025 Conference Paper

A Probabilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction

Leander Kurscheidt
Paolo Morettin
Roberto Sebastiani
Andrea Passerini
Antonio Vergari

In safety-critical applications, guaranteeing the satisfaction of constraints over continuous environments is crucial, e. g. , an autonomous agent should never crash over obstacles or go off-road. Neural models struggle in the presence of these constraints, especially when they involve intricate algebraic relationships. To address this, we introduce a differentiable probabilistic layer that guarantees the satisfaction of non-convex algebraic constraints over continuous variables. This probabilistic algebraic layer (PAL) can be seamlessly plugged into any neural architecture and trained via maximum likelihood without requiring approximations. PAL defines a distribution over conjunctions and disjunctions of linear inequalities, parametrized by polynomials. This formulation enables efficient and exact renormalization via symbolic integration, which can be amortized across different data points and easily parallelized on a GPU. We showcase PAL and our integration scheme on a number of benchmarks for algebraic constraint integration and on real-world trajectory data.

Details

AIJ Journal 2025 Journal Article

Disjoint projected enumeration for SAT and SMT without blocking clauses

Giuseppe Spallitta
Roberto Sebastiani
Armin Biere

All-Solution Satisfiability (AllSAT) and its extension, All-Solution Satisfiability Modulo Theories (AllSMT), have become more relevant in recent years, mainly in formal verification and artificial intelligence applications. The goal of these problems is the enumeration of all satisfying assignments of a formula (for SAT and SMT problems, respectively), making them useful for test generation, model checking, and probabilistic inference. Nevertheless, traditional AllSAT algorithms face significant computational challenges due to the exponential growth of the search space and inefficiencies caused by blocking clauses, which cause memory blowups and degrade unit propagation performance in the long term. This paper presents two novel solvers: TABULARALLSAT, a projected AllSAT solver, and TABULARALLSMT, a projected AllSMT solver. Both solvers combine Conflict-Driven Clause Learning (CDCL) with chronological backtracking to improve efficiency while ensuring disjoint enumeration. To retrieve compact partial assignments we propose a novel aggressive implicant shrinking algorithm, compatible with chronological backtracking, to minimize the number of partial assignments, reducing overall search complexity. Furthermore, we extend the solver framework to handle projected enumeration and SMT formulas effectively and efficiently, adapting the baseline framework to integrate theory reasoning and the distinction between important and non-important variables. An extensive experimental evaluation demonstrates the superiority of our approach compared to state-of-the-art solvers, particularly in scenarios requiring projection and SMT-based reasoning.

Details DOI

JAIR Journal 2025 Journal Article

On CNF Conversion for SAT and SMT Enumeration

Gabriele Masina
Giuseppe Spallitta
Roberto Sebastiani

Modern SAT and SMT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants of either Tseitin or Plaisted and Greenbaum transformations. When passing from plain solving to enumeration, however, the capability of producing partial satisfying assignments that are as small as possible becomes crucial, which raises the question of whether such CNF encodings are also effective for enumeration. In this paper, we investigate both theoretically and empirically the effectiveness of CNF conversions for SAT and SMT enumeration. On the negative side, we show that: (i) Tseitin transformation prevents the solver from producing short partial assignments, thus seriously affecting the effectiveness of enumeration; (ii) Plaisted and Greenbaum transformation overcomes this problem only in part. On the positive side, we prove theoretically and we show empirically that combining Plaisted and Greenbaum transformation with NNF preprocessing upfront —which is typically not used in solving— can fully overcome the problem and can drastically reduce both the number of partial assignments and the execution time.

PDF Details DOI

ECAI Conference 2024 Conference Paper

Canonical Decision Diagrams Modulo Theories

Massimo Michelutti
Gabriele Masina
Giuseppe Spallitta
Roberto Sebastiani

Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e. g. , OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. Given the limited expressiveness of propositional logic, a few attempts to leverage DDs to SMT level have been presented in the literature. Unfortunately, these techniques still suffer from some limitations: most procedures are theory-specific; some produce theory DDs (T-DDs) which do not univocally represent T-valid formulas or T-inconsistent formulas; none of these techniques provably produces theory-canonical T-DDs, which (under given conditions on the T-atom list) univocally represent T-equivalence classes of formulas. Also, these procedures are not easy to implement, and very few implementations are actually available. In this paper, we present a novel very-general technique to leverage DDs to SMT level, which has several advantages: it is very easy to implement on top of an AllSMT solver and a DD package, which are used as black boxes; it works for every form of DDs and every theory, or combination thereof, supported by the AllSMT solver; it produces theory-canonical T-DDs if the propositional DD is canonical. We have implemented a prototype tool for both T-OBDDs and T-SDDs on top of OBDD and SDD packages and the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.

Details

AAAI Conference 2024 Conference Paper

Disjoint Partial Enumeration without Blocking Clauses

Giuseppe Spallitta
Roberto Sebastiani
Armin Biere

A basic algorithm for enumerating disjoint propositional models (disjoint AllSAT) is based on adding blocking clauses incrementally, ruling out previously found models. On the one hand, blocking clauses have the potential to reduce the number of generated models exponentially, as they can handle partial models. On the other hand, the introduction of a large number of blocking clauses affects memory consumption and drastically slows down unit propagation. We propose a new approach that allows for enumerating disjoint partial models with no need for blocking clauses by integrating: Conflict-Driven Clause-Learning (CDCL), Chronological Backtracking (CB), and methods for shrinking models (Implicant Shrinking). Experiments clearly show the benefits of our novel approach.

PDF Details DOI

AIJ Journal 2024 Journal Article

Enhancing SMT-based Weighted Model Integration by structure awareness

Giuseppe Spallitta
Gabriele Masina
Paolo Morettin
Andrea Passerini
Roberto Sebastiani

The development of efficient exact and approximate algorithms for probabilistic inference is a long-standing goal of artificial intelligence research. Whereas substantial progress has been made in dealing with purely discrete or purely continuous domains, adapting the developed solutions to tackle hybrid domains, characterized by discrete and continuous variables and their relationships, is highly non-trivial. Weighted Model Integration (WMI) recently emerged as a unifying formalism for probabilistic inference in hybrid domains. Despite a considerable amount of recent work, allowing WMI algorithms to scale with the complexity of the hybrid problem is still a challenge. In this paper we highlight some substantial limitations of existing state-of-the-art solutions, and develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in drastic computational savings. Additionally, we show how SMT-based approaches can seamlessly deal with different integration techniques, both exact and approximate, significantly expanding the set of problems that can be tackled by WMI technology. An extensive experimental evaluation on both synthetic and real-world datasets confirms the substantial advantage of the proposed solution over existing alternatives. The application potential of this technology is further showcased on a prototypical task aimed at verifying the fairness of probabilistic programs.

Details DOI

SAT Conference 2024 Conference Paper

Entailing Generalization Boosts Enumeration

Dror Fried
Alexander Nadel
Roberto Sebastiani
Yogev Shalmon

Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.

Details

SAT Conference 2023 Conference Paper

On CNF Conversion for Disjoint SAT Enumeration

Gabriele Masina
Giuseppe Spallitta
Roberto Sebastiani

Modern SAT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants of either Tseitin or Plaisted and Greenbaum transformations. When passing from solving to enumeration, however, the capability of producing partial satisfying assignments that are as small as possible becomes crucial, which raises the question of whether such CNF encodings are also effective for enumeration. In this paper, we investigate both theoretically and empirically the effectiveness of CNF conversions for disjoint SAT enumeration. On the negative side, we show that: (i) Tseitin transformation prevents the solver from producing short partial assignments, thus seriously affecting the effectiveness of enumeration; (ii) Plaisted and Greenbaum transformation overcomes this problem only in part. On the positive side, we show that combining Plaisted and Greenbaum transformation with NNF preprocessing upfront - which is typically not used in solving - can fully overcome the problem and can drastically reduce both the number of partial assignments and the execution time.

Details

UAI Conference 2022 Conference Paper

SMT-based weighted model integration with structure awareness

Giuseppe Spallitta
Gabriele Masina
Paolo Morettin
Andrea Passerini
Roberto Sebastiani

Weighted Model Integration (WMI) is a popular formalism aimed at unifying approaches for probabilistic inference in hybrid domains, involving logical and algebraic constraints. Despite a considerable amount of recent work, allowing WMI algorithms to scale with the complexity of the hybrid problem is still a challenge. In this paper we highlight some substantial limitations of existing state-of-the-art solutions, and develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in substantial computational savings. An extensive experimental evaluation on both synthetic and real-world datasets confirms the advantage of the proposed solution over existing alternatives.

Details

SAT Conference 2020 Conference Paper

Four Flavors of Entailment

Sibylle Möhle
Roberto Sebastiani
Armin Biere

Abstract We present a novel approach for enumerating partial models of a propositional formula, inspired by how theory solvers and the SAT solver interact in lazy SMT. Using various forms of dual reasoning allows our CDCL-based algorithm to enumerate partial models with no need for exploring and shrinking full models. Our focus is on model enumeration without repetition, with potential applications in weighted model counting and weighted model integration for probabilistic inference over Boolean and hybrid domains. Chronological backtracking renders the use of blocking clauses obsolete. We provide a formalization and examples. We further discuss important design choices for a future implementation related to the strength of dual reasoning, including unit propagation, using SAT or QBF oracles.

Details

I&C Journal 2020 Journal Article

Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results

Zhengbing Bian
Fabian Chudak
William Macready
Aidan Roy
Roberto Sebastiani
Stefano Varotti

Quantum annealers (QAs) are specialized quantum computers that minimize objective functions over discrete variables by physically exploiting quantum effects. Current QA platforms allow for the optimization of quadratic objectives defined over binary variables (qubits), also known as Ising problems. In the last decade, QA systems as implemented by D-Wave have scaled with Moore-like growth. Current architectures provide 2048 sparsely-connected qubits, and continued exponential growth is anticipated, together with increased connectivity. We explore the feasibility of such architectures for solving SAT and MaxSAT problems as QA systems scale. We develop techniques for effectively encoding SAT –and, with some limitations, MaxSAT– into Ising problems compatible with sparse QA architectures. We provide the theoretical foundations for this mapping, and present encoding techniques that combine offline Satisfiability and Optimization Modulo Theories with on-the-fly placement and routing. Preliminary empirical tests on a current generation 2048-qubit D-Wave system support the feasibility of the approach for certain SAT and MaxSAT problems.

Details DOI

AIJ Journal 2019 Journal Article

Advanced SMT techniques for weighted model integration

Paolo Morettin
Andrea Passerini
Roberto Sebastiani

Weighted model integration (WMI) is a recent formalism generalizing weighted model counting (WMC) to run probabilistic inference over hybrid domains, characterized by both discrete and continuous variables and relationships between them. WMI is computationally very demanding as it requires to explicitly enumerate all possible truth assignments to be integrated over. Component caching strategies which proved extremely effective for WMC are difficult to apply in this formalism because of the tight coupling induced by the arithmetic constraints. In this paper we present a novel formulation of WMI, which allows to exploit the power of SMT-based predicate abstraction techniques in designing efficient inference procedures. A novel algorithm combines a strong reduction in the number of models to be integrated over with their efficient enumeration. Experimental results on synthetic and real-world data show drastic computational improvements over the original WMI formulation as well as existing alternatives for hybrid inference.

Details DOI

IJCAI Conference 2019 Conference Paper

The pywmi Framework and Toolbox for Probabilistic Inference using Weighted Model Integration

Samuel Kolb
Paolo Morettin
Pedro Zuidberg Dos Martires
Francesco Sommavilla
Andrea Passerini
Roberto Sebastiani
Luc De Raedt

Weighted Model Integration (WMI) is a popular technique for probabilistic inference that extends Weighted Model Counting (WMC) -- the standard inference technique for inference in discrete domains -- to domains with both discrete and continuous variables. However, existing WMI solvers each have different interfaces and use different formats for representing WMI problems. Therefore, we introduce pywmi (http: //pywmi. org), an open source framework and toolbox for probabilistic inference using WMI, to address these shortcomings. Crucially, pywmi fixes a common internal format for WMI problems and introduces a common interface for WMI solvers. To assist users in modeling WMI problems, pywmi introduces modeling languages based on SMT-LIB. v2 or MiniZinc and parsers for both. To assist users in comparing WMI solvers, pywmi includes implementations of several state-of-the-art solvers, a fast approximate WMI solver, and a command-line interface to solve WMI problems. Finally, to assist developers in implementing new solvers, pywmi provides Python implementations of commonly used subroutines.

PDF Details

SAT Conference 2018 Conference Paper

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization

Alessandro Cimatti
Alberto Griggio
Ahmed Irfan
Marco Roveri
Roberto Sebastiani

Abstract Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its effectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

Details

IJCAI Conference 2017 Conference Paper

Efficient Weighted Model Integration via SMT-Based Predicate Abstraction

Paolo Morettin
Andrea Passerini
Roberto Sebastiani

Weighted model integration (WMI) is a recent formalism generalizing weighted model counting (WMC) to run probabilistic inference over hybrid domains, characterized by both discrete and continuous variables and relationships between them. Albeit powerful, the original formulation of WMI suffers from some theoretical limitations, and it is computationally very demanding as it requires to explicitly enumerate all possible models to be integrated over. In this paper we present a novel general notion of WMI, which fixes the theoretical limitations and allows for exploiting the power of SMT-based predicate abstraction techniques. A novel algorithm combines a strong reduction in the number of models to be integrated over with their efficient enumeration. Experimental results on synthetic and real-world data show drastic computational improvements over the original WMI formulation as well as existing alternatives for hybrid inference.

PDF Details

AIJ Journal 2017 Journal Article

Structured learning modulo theories

Stefano Teso
Roberto Sebastiani
Andrea Passerini

Modeling problems containing a mixture of Boolean and numerical variables is a long-standing interest of Artificial Intelligence. However, performing inference and learning in hybrid domains is a particularly daunting task. The ability to model these kinds of domains is crucial in “learning to design” tasks, that is, learning applications where the goal is to learn from examples how to perform automatic de novo design of novel objects. In this paper we present Structured Learning Modulo Theories, a max-margin approach for learning in hybrid domains based on Satisfiability Modulo Theories, which allows to combine Boolean reasoning and optimization over continuous linear arithmetical constraints. The main idea is to leverage a state-of-the-art generalized Satisfiability Modulo Theory solver for implementing the inference and separation oracles of Structured Output SVMs. We validate our method on artificial and real world scenarios.

Details DOI

SAT Conference 2013 Conference Paper

A Modular Approach to MaxSAT Modulo Theories

Alessandro Cimatti
Alberto Griggio
Bastiaan Joost Schaafsma
Roberto Sebastiani

Abstract In this paper we present a novel “modular” approach for (weighted partial) MaxSAT Modulo Theories. The main idea is to combine a lazy SMT solver with a purely-propositional (weighted partial) MaxSAT solver, by making them exchange information iteratively: the former produces an increasing set of theory lemmas which are used by the latter to progressively refine an approximation of the final subset of the soft clauses, which is eventually returned as output. The approach has several practical features. First, it is independent from the theories addressed. Second, it is simple to implement and to update, since both SMT and MaxSAT solvers can be used as blackboxes. Third, it can be interfaced with external MaxSAT and SMT solvers in a plug-and-play manner, so that to benefit for free of tools which are or will be made available. We have implemented our approach on top of the MathSAT5 SMT solver and of a selection of external MaxSAT solvers, and we have evaluated it by means of an extensive empirical test on SMT-LIB benchmarks. The results confirm the validity and potential of this approach.

Details

SAT Conference 2007 Conference Paper

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories

Alessandro Cimatti
Alberto Griggio
Roberto Sebastiani

Abstract Finding small unsatisfiable cores for SAT problems has recently received a lot of interest, mostly for its applications in formal verification. Surprisingly, the same problem in the context of SAT Modulo Theories (SMT) has instead received very little attention in the literature; in particular, we are not aware of any work aiming at producing small unsatisfiable cores in SMT. The purpose of this paper is to start filling the gap in this area, by proposing a novel approach for computing small unsat cores in SMT. The main idea is to combine an SMT solver with an external propositional core extractor: the SMT solver produces the theory lemmas found during the search; the core extractor is then called on the boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas have been removed. The approach has several advantages: it is extremely simple to implement and to update, and it can be interfaced with every propositional core extractor in a plug-and-play way, so that to benefit for free of all unsat-core reduction techniques which have been or will be made available.

Details

LPAR Conference 2006 Conference Paper

Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis

Roberto Bruttomesso
Alessandro Cimatti
Anders Franzén
Alberto Griggio
Roberto Sebastiani

Abstract Many approaches for Satisfiability Modulo Theory ( SMT \({\mathcal({T})})\) rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory \({\mathcal{T}} ({\mathcal{T}}-solver\) ). When \({\mathcal{T}}\) is the combination \({{\mathcal{T}}_1\cup{\mathcal{T}}_2}\) of two simpler theories, the approach is typically handled by means of Nelson-Oppen’s (NO) theory combination schema in which two specific \({\mathcal{T}}\) - solver deduce and exchange (disjunctions of) interface equalities. In recent papers we have proposed a new approach to \(({{\mathcal{T}}_1\cup{\mathcal{T}}_2})\), called Delayed Theory Combination ( Dtc ). Here part or all the (possibly very expensive) task of deducing interface equalities is played by the SAT solver itself, at the potential cost of an enlargement of the boolean search space. In principle this enlargement could be up to exponential in the number of interface equalities generated. In this paper we show that this estimate was too pessimistic. We present a comparative analysis of Dtc vs. NO for SMT \(({{\mathcal{T}}_1\cup{\mathcal{T}}_2})\), which shows that, using state-of-the-art SAT-solving techniques, the amount of boolean branches performed by Dtc can be upper bounded by the number of deductions and boolean branches performed by NO on the same problem. We prove the result for different deduction capabilities of the \({\mathcal({T}-solver)}\) and for both convex and non-convex theories.

Details

I&C Journal 2006 Journal Article

Efficient theory combination via boolean search

Marco Bozzano
Roberto Bruttomesso
Alessandro Cimatti
Tommi Junttila
Silvio Ranise
Peter van Rossum
Roberto Sebastiani

Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T—also known as Satisfiability Modulo Theory, or SMT(T)—rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory T is the combination T 1 ∪ T 2 of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e. g. Nelson–Oppen, Shostak). In this paper we propose a new approach to SMT ( T 1 ∪ T 2 ), where the enumerator of truth assignments is integrated with two decision procedures, one for T 1 and one for T 2, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i. e. , cheaper reasoning first, and more often). We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions ( EUF ) and Linear Arithmetic ( LA ), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance.

Details DOI

SAT Conference 2006 Conference Paper

Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC

Roberto Sebastiani
Michele Vescovi

Abstract In the last two decades, modal and description logics have been applied to numerous areas of computer science, including artificial intelligence, formal verification, database theory, and distributed computing. For this reason, the problem of automated reasoning in modal and description logics has been throughly investigated. In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic K m, and of its notational variant, the description logic \(\ensuremath{\mathcal{ALC}}\). Although simple in structure, K m / \(\ensuremath{\mathcal{ALC}}\) is computationally very hard to reason on, its satisfiability being PSPACE-complete. In this paper we explore the idea of encoding K m / \(\ensuremath{\mathcal{ALC}}\) -satisfiability into SAT, so that to be handled by state-of-the-art SAT tools. We propose an efficient encoding, and we test it on an extensive set of benchmarks, comparing the approach with the main state-of-the-art tools available. Although the encoding is necessarily worst-case exponential, from our experiments we notice that, in practice, this approach can handle most or all the problems which are at the reach of the other approaches, with performances which are comparable with, or even better than, those of the current state-of-the-art tools.

Details

LPAR Conference 2006 Conference Paper

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT ( EUF È T )

Roberto Bruttomesso
Alessandro Cimatti
Anders Franzén
Alberto Griggio
Alessandro Santuari
Roberto Sebastiani

Abstract Satisfiability Modulo Theories \((\mathit{SMT}(\mathcal{T}))\) is the problem of deciding the satisfiability of a formula with respect to a given background theory \({\mathcal{T}}\). When \({\mathcal{T}}\) is the combination of two simpler theories \({{\mathcal{T}}_1}\) and \({{\mathcal{T}}_2} ({\mathit{SMT}({{\mathcal{T}}_1\cup{\mathcal{T}}_2})})\), a standard and general approach is to handle the integration of \({{\mathcal{T}}_1}\) and \({{\mathcal{T}}_2}\) by performing some form of search on the equalities between the shared variables. A frequent and very relevant sub-case of \({\mathit{SMT}({{\mathcal{T}}_1\cup{\mathcal{T}}_2})}\) is when \({{\mathcal{T}}_1}\) is the theory of Equality and Uninterpreted Functions \(({\mathcal{EUF}})\). For this case, an alternative approach is to eliminate first all uninterpreted function symbols by means of Ackermann’s expansion, and then to solve the resulting \({\mathit{SMT}}({{\mathcal{T}}_2})\) problem. In this paper we build on the empirical observation that there is no absolute winner between these two alternative approaches, and that the performance gaps between them are often dramatic, in either direction. We propose a simple technique for estimating a priori the costs and benefits, in terms of the size of the search space of an \({\mathit{SMT}}\) tool, of applying Ackermann’s expansion to all or part of the function symbols. A thorough experimental analysis, including the benchmarks of the SMT’05 competition, shows that the proposed technique is extremely effective in improving the overall performance of the \({\mathit{SMT}}\) tool.

Details

EAAI Journal 2005 Journal Article

Goal-oriented requirements analysis and reasoning in the Tropos methodology

Paolo Giorgini
John Mylopoulos
Roberto Sebastiani

Tropos is an agent-oriented software methodology proposed in (J. Autonomous Agents Multi-Agent Syst. 8(3) (2004) 203; Inf. Syst. 27(6) (2002) 365). The methodology is founded on the notions of agent and goal, and goal analysis is used extensively to support software development during different phases. This paper adopts a formal goal model defined and analyzed in (J. Data Semantics 1 (2003); Proceedings of the International Conference on Advanced Information Systems Engineering, CAISE’04, vol. 3804 of LNCS, Springer, Berlin, 2004, pp. 20–33) to make the goal analysis process concrete through the use of forward and backward reasoning for goal models. The formal goal analysis is illustrated through examples, using an implemented goal reasoning tool.

Details DOI

I&C Journal 2000 Journal Article

Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m)

Fausto Giunchiglia
Roberto Sebastiani

The goal of this paper is to propose a new technique for developing decision procedures for propositional modal logics. The basic idea is that propositional modal decision procedures should be developed on top of propositional decision procedures. As a case study, we consider satisfiability in modal K(m), that is modal K with m modalities, and develop an algorithm, called K SAT, on top of an implementation of the Davis–Putnam–Longemann–Loveland procedure. K SAT is thoroughly tested and compared with various procedures and in particular with the state-of-the-art tableau-based system K RIS. The experimental results show that K SAT outperforms K RIS and the other systems of orders of magnitude, highlight an intrinsic weakness of tableau-based decision procedures, and provide partial evidence of a phase transition phenomenon for K(m).

Details DOI

AAAI Conference 1996 Conference Paper

Computing Abstraction Hierarchies by Numerical Simulation

Alan Bundy
Roberto Sebastiani

We present a novel method for building ABSTRIPSstyle abstraction hierarchies in planning. The aim of this method is to minimize the amount of backtracking between abstraction levels. Previous approaches have determined the criticality of operator preconditions by reasoning about plans directly. Here, we adopt a simpler and faster approach where we use numerical simulation of the planning process. We demonstrate the theoretical advantages of our approach by identifying some simple properties lacking in previous approaches but possessed by our method. We demonstrate the empirical advantages of our approach by a set of four benchmark experiments using the ABTWEAK system. We compare the quality of the abstraction hierarchies generated with those built by the ALPINE and HIGHPOINT algorithms.

PDF Details