Cesare Tinelli

Department of Computer Science

University of Iowa

USA

(Extended and improved version of [NOT04].)

Abstract.We first introduce Abstract DPLL, a rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason about them in a simple way. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as backjumping or clause learning.

We then extend the framework to Satisfiability Modulo background Theories (SMT) and use it to model several variants of the so-called lazy approach for SMT. In particular, we use it to introduce a few variants of a new, efficient and modular approach for SMT based on a general DPLL(X) engine, whose parameter X can be instantiated with a specialized solver Solver_T for a given theory T, thus producing a DPLL(T) system. We describe the high level design of DPLL(X) and its cooperation with Solver_T, discuss the role of theory propagation, and show how to implement DPLL(T) for some theories arising in industrial applications.

Our extensive experimental evidence, summarized in this paper, shows that DPLL(T) systems can significantly outperform the other state-of-the-art tools, frequently even in orders of magnitude, and have better scaling properties.

Peter Baumgartner and Cesare Tinelli.

(Extended and improved version of [BT03].) 2005.

Abstract.The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment of universal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.

Silvio Ranise and Cesare Tinelli.

Abstract.The SMT-LIB initiative is an international effort, coordinated by these authors and supported by several research groups world-wide, with the main goal of producing an extensive on-line library of benchmarks forsatisfiability modulo theories. This paper defines syntax and semantics of the language used by SMT-LIB for writing theory specifications and benchmarks.

(Extended version of [BGT04].)

Abstract.Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics---which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories.

In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.

Peter Baumgartner, Alexander Fuchs, Hans de Nivelle, and Cesare Tinelli.

Abstract.Recent years have seen considerable interest in procedures for computing finite models of first-order logic specifications. One of the major paradigms, MACE-style model building, is based on reducing model search to a sequence of propositional satisfiability problems and applying (efficient) SAT solvers to them. A problem with this method is that it does not scale well, as the propositional formulas to be considered may become very large.

We propose instead to reduce model search to a sequence of satisfiability problems made of function-free first-order clause sets, and to apply (efficient) theorem provers capable of deciding such problems. The main appeal of this method is that first-order clause sets grow more slowly than their propositional counterparts, thus allowing for more space efficient reasoning.

In the paper we describe the method in detail and show how it is integrated into one such prover, Darwin, our implementation of the Model Evolution calculus. The results are general, however, as our approach can be used in principle with any system that decides the satisfiability of function-free first-order clause sets.

To demonstrate its practical feasibility, we tested our approach on all satisfiable problems from the TPTP library. Our methods can solve a significant subset of these problems, which overlaps but is not included in the subset of problems solvable by state-of-the-art finite model builders such as Paradox and Mace4.

Cesare Tinelli and Calogero Zarba.

(Extended and amended version of [TZ03].)

Abstract.The Nelson-Oppen combination method combines decision procedures for first-order theories over disjoint signatures into a single decision procedure for the union theory. To be correct, the method requires that the component theories be stably infinite. This restriction makes the method inapplicable to many interesting theories such as, for instance, theories having only finite models. In this paper, we describe two extensions of the Nelson-Oppen method that address the problem of combining theories that are not stably infinite. In our extensions, the component decision procedures exchange not only equalities between shared variables, but also certain cardinality constraints. Applications of our results include the combination of theories having only finite models, as well as the combination of non-stably infinite theories with the theory of equality, the theories of total and partial orders, and the theory of lattices with maximum and minimum.

Peter Baumgartner, Alexander Fuchs and Cesare Tinelli.

(Extended version of [BFT04].)

Abstract.Darwin is the first implementation of the Model Evolution Calculus by Baumgartner and Tinelli. The Model Evolution Calculus lifts the DPLL procedure to first-order logic. Darwin is meant to be a fast and clean implementation of the calculus, showing its effectiveness and providing a base for further improvements and extensions. Based on a brief summary of the Model Evolution Calculus, we describe in the main part of the paper Darwin's proof procedure and its data structures and algorithms, discussing the main design decisions and features that influence Darwin's performance. We also report on practical experiments carried out with problems from the CASC-J2 system competition and parts of the TPTP Problem Library, and compare the results with those of other state-of-the-art theorem provers.

Peter Baumgartner and Cesare Tinelli.

Abstract.In many theorem proving applications, a proper treatment of equa- tional theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the Model Evolution calculus (ME), a first- order version of the propositional DPLL procedure. The new calculus, ME_E , is a proper extension of the ME calculus without equality. Like ME it maintains an explicit candidate model, which is searched for by DPLL-style splitting. For equational reasoning ME_E uses an adapted version of the ordered paramodu- lation inference rule, where equations used for paramodulation are drawn (only) from the candidate model. The calculus also features a generic, semantically justi- fied simplification rule which covers many simplification techniques known from superposition-style theorem proving. Our main result is the correctness of the ME_E calculus in the presence of very general redundancy elimination criteria.

Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.

Abstract.We introduceAbstract DPLL, a general and simple abstract rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as non-chronological backtracking or clause learning. This allows one to formally reason about practical DPLL algorithms in a simple way. In the second part of this paper we extend the framework toAbstract DPLL modulo theories. This allows us to express---and formally reason about---state-of-the-art concrete DPLL-based techniques for satisfiability modulo background theories, such as the differentlazyapproaches, or our DPLL(T) framework.

Cesare Tinelli and Calogero Zarba.

Abstract.The Nelson-Oppen combination method combines decision procedures for theories satisfying certain conditions into a decision procedure for their union. While the method is known to be correct in the setting of unsorted first-order logic, some current implementations of it appear in tools that use a sorted input language. So far, however, there have been no theoretical results on the correctness of the method in a sorted setting, nor is it obvious that the method in fact lifts as is to logics with sorts. To bridge this gap between the existing theoretical results and the current implementations, we extend the Nelson-Oppen method to (order-)sorted logic and prove it correct under conditions similar to the original ones. From a theoretical point of view, the extension is relevant because it provides a rigorous foundation for the application of the method in a sorted setting. From a practical point of view, the extension has the considerable added benefits that in a sorted setting the method's preconditions become easier to satisfy in practice, and the method's nondeterminism is generally reduced.

Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.

Abstract.The logic of equality with uninterpreted functions and its extensions have been widely applied to processor verification, by means of a large variety of progressively more sophisticated (lazy or eager) translations into propositional SAT. Here we propose a new approach, namely a general DPLL(X) engine, whose parameter X can be instantiated with a specialized solver for a given theory T, thus producing a system DPLL(T). We decribe this DPLL(T) scheme, the interface between DPLL(X) and the theory solver, the architecture of DPLL(X), and our solver for EUF, which includes incremental and backtrackable congruence closure algorithms for dealing with the built-in equality and the integer successor and predecessor symbols. Experiments with a first implementation indicate that our technique already outperforms the previous methods on most benchmarks, and scales up very well.

Franz Baader, Silvio Ghilardi and Cesare Tinelli.

Abstract.Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics---which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories.

In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.

Peter Baumgartner and Cesare Tinelli.

Abstract.The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment ofuniversal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.

Cesare Tinelli and Calogero Zarba.

Abstract.The Nelson-Oppen combination method combines decision procedures for first-order theories over disjoint signatures into a single decision procedure for the union theory. To be correct, the method requires that the component theories be stably infinite. This restriction makes the method inapplicable to many interesting theories such as, for instance, theories having only finite models. In this paper we provide a new combination method that can combine any theory that is not stably infinite with another theory, provided that the latter is what we call ashinytheory. Examples of shiny theories include the theory of equality, the theory of partial orders, and the theory of total orders. An interesting consequence of our results is that any decision procedure for the satisfiability of quantifier-free Σ-formulae in a Σ-theoryTcan always be extended to accept inputs over an arbitrary signature Ω ⊇ Σ.

Cesare Tinelli.

Abstract.We propose a general way of combining background reasoners in theory reasoning. Using a restricted version of the Craig Interpolation Lemma, we show that background reasoner cooperation can be achieved as a form of constraint propagation, much in the spirit of existing combination methods for decision procedures. In this case, constraint information is propagated across reasoners by exchangingresiduesthat are, in essence, disjunctions of ground literals over a common signature. As an application of our approach, we describe a multi-theory version of the semantic tableau calculus and we prove it sound and complete.

Cesare Tinelli and Christophe Ringeissen.

Abstract.In this paper we outline a theoretical framework for the combination of decision procedures for constraint satisfiability. We describe a general combination method which, given a procedure that decides constraint satisfiability with respect to a constraint theory T_1 and one that decides constraint satisfiability with respect to a constraint theory T_2, produces a procedure that (semi-)decides constraint satisfiability with respect to the union of T_1 and T_2. We provide a number of model-theoretic conditions on the constraint language and the component constraint theories for the method to be sound and complete, with special emphasis on the case in which the signatures of the component theories are non-disjoint. We also describe possible applications of the method and relate it to some of the existing combination methods in the field.

Franz Baader and Cesare Tinelli.

Abstract.The main contribution of this paper is a new method for combining decision procedures for the word problem in equational theories. In contrast to previous methods, this method is based on transformation rules. Furthermore, it is not limited to theories with disjoint signatures but it also applies to theories sharingconstructors.

Cesare Tinelli.

Abstract.We describe and discuss DPLL(T), a parametric calculus for proving the satisfiability of ground formulas in a logical theory T. The calculus tightly integrates a decision procedure for the satisfiability in T of sets of literals into a sequent calculus based on the well-known method by Davis, Putman, Logemann and Loveland for proving the satisfiability of propositional formulas. For being based on the DPLL method, DPLL(T) can incorporate a number of very effective search heuristics developed by the SAT community for that method. Hence, it can be used as the formal basis for novel and efficient implementations of satisfiability checkers for theories with decidable ground consequences.

Franz Baader and Cesare Tinelli.

Abstract.This paper addresses the following combination problem: given two equational theories E_1 and E_2 whose positive theories are decidable, how can one obtain a decision procedure for the positive theory of E_1 U E_2? For theories over disjoint signatures, this problem was solved by Baader and Schulz in 1995. This paper is a first step towards extending this result to the case of theories sharing constructors. Since there is a close connection between positive theories and unification problems, this also extends to the non-disjoint case the work on combining decision procedures for unification modulo equational theories.

Cesare Tinelli.

Abstract.We propose a general way of combining background reasoners in theory reasoning. Using a restricted version of the Craig Interpolation Lemma, we show that background reasoner cooperation can be achieved as a form of constraint propagation, much in the spirit of existing combination methods for decision procedures. In this case, constraint information is propagated across reasoners by exchangingresiduesover a common signature. As an application of our approach, we describe a multi-theory version of the semantic tableau calculus.

Franz Baader and Cesare Tinelli.

Abstract.In this paper we extend the applicability of our combination method for decision procedures for the word problem to theories sharingnon-collapse-freeconstructors. This extension broadens the scope of the combination procedure considerably, for example in the direction of equational theories axiomatizing the equivalence of modal formulae.

Franz Baader and Cesare Tinelli.

Abstract.The main contribution of this paper is a new method for combining decision procedures for the word problem in equational theories sharing ``constructors.'' The notion of constructor adopted in this paper has a nice algebraic definition and is more general than a related notion introduced in previous work on the combination problem.

Cesare Tinelli and Mehdi Harandi.

Abstract.In this paper, we present an extension of the Jaffar-Lassez Constraint Logic Programming scheme that operates with unions of constraint theories with different signatures and decides the satisfiability ofmixedconstraints by appropriately combining the constraint solvers of the component theories. We describe the extended scheme and provide logical and operational semantics for it along the lines of those given for the original scheme. We then show how the main soundness and completeness results of Constraint Logic Programming lift to our extension.

Franz Baader and Cesare Tinelli.

Abstract.The Nelson-Oppen combination method can be used to combine decision procedures for the validity of quantifier-free formulae in first-order theories with disjoint signatures, provided that the theories to be combined are stably infinite. We show that, even though equational theories need not satisfy this property, Nelson and Oppen's method can be applied, after some minor modifications, to combine decision procedures for the validity of quantifier-free formulae in equational theories. Unfortunately, and contrary to a common belief, the method cannot be used to combine decision procedures for the word problem. We present a method that solves this kind of combination problem. Our method is based on transformation rules and also applies to equational theories that share a finite number of constant symbols.

Cesare Tinelli and Mehdi Harandi.

Abstract.In this paper, we propose an extension of the Jaffar-Lassez Constraint Logic Programming scheme that operates with unions of constraint theories with different signatures and decides the satisfiability ofmixedconstraints by appropriately combining the constraint solvers of the component theories. We describe the extended scheme and provide logical and operational semantics for it along the lines of those given for the original scheme. Then we show how the main soundness and completeness results of Constraint Logic Programming lift to our extension.

Cesare Tinelli and Mehdi Harandi

Abstract.The Nelson-Oppen combination procedure, which combines satisfiability procedures for a class of first-order theories by propagation of equalities between variables, is one of the most general combination methods in the field of theory combination. We describe a new non-deterministic version of the procedure that has been used to extend the Constraint Logic Programming Scheme to unions of constraint theories. The correctness proof of the procedure that we give in this paper not only constitutes a novel and easier proof of Nelson and Oppen's original results, but also shows that equality sharing between the satisfiability procedures of the component theories, the main idea of the method, can be confined to a restricted set of variables. While working on the new correctness proof, we also found a new characterization of the consistency of the union of first-order theories. We discuss and give a proof of such characterization as well.

Abstract.The theory of recursive data types is a valuable modeling tool for software verification. In the past, decision procedures have been proposed for both the full theory and its universal fragment. However, previous work has been limited in various ways, including an inability to deal with multiple constructors, multi-sorted logic, and mutually recursive data types. More significantly, previous algorithms for the universal case have been based on inefficient nondeterministic guesses and have been described in fairly complex procedural terms. We present an algorithm which addresses these issues for the universal theory. The algorithm is presented declaratively as a set of abstract rules which are terminating, sound, and complete. We also describe strategies for applying the rules and explain why our recommended strategy is more efficient than those used by previous algorithms. Finally, we discuss how the algorithm can be used within a broader framework of cooperating decision procedures.

Vijay Ganesh, Sergey Berezin, Cesare Tinelli, David L. Dill.

Abstract.We present a combination result for many-sorted first-order theories whose signatures may share common symbols. A direct consequence of this result is the extension of the first-order (unsorted) Nelson-Oppen combination method to the many-sorted case. Furthermore, we provide several sufficient conditions under which the combinati on of two theories with overlapping signatures is decidable. We also provide some practical sufficiency conditions under which the union of theories is consistent and the combination method is complete. These results provide a theoretical basis for establishing the correctness of the CVC Lite tool and its extension to theories with overlapping signatures.

Cesare Tinelli and Calogero Zarba.

Abstract.The Nelson-Oppen combination method combines decision procedures for theories satisfying certain conditions into a decision procedure for their union. While the method is known to be correct in the setting of unsorted first-order logic, several current implementations of it appear in tools that use a sorted input language. So far, however, there have been no theoretical results on the correctness of the method in a sorted setting, nor it is obvious that the method in fact lifts as is to logics with sorts. To bridge this gap between the existing theoretical results and the current implementations, we extend the Nelson-Oppen method to (order-)sorted logic and prove it correct under conditions similar to the original ones. From a theoretical standpoint, the extension is relevant because it finally provides a rigorous foundation for the application of the method in a sorted setting. From a practical standpoint, the extension has the considerable added benefits that in a sorted setting the method's preconditions become easier to satify in practice, and the method's nondeterminism is generally reduced.

Franz Baader, Silvio Ghilardi and Cesare Tinelli.

Abstract.Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics---which are not disjoint for sharing the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other types of equational theories.

In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.

Peter Baumgartner and Cesare Tinelli.

Abstract.The DPLL procedure is the basis of some of the most successful propositional satisfiability solvers to date. Although originally devised as a proof-procedure for first-order logic, it has been used almost exclusively for propositional logic so far because of its highly inefficient treatment of quantifiers, based on instantiation into ground formulas. The recent FDPLL calculus by Baumgartner was the first successful attempt to lift the procedure to the first-order level without resorting to ground instantiations. FDPLL lifts to the first-order case the core of the DPLL procedure, the splitting rule, but ignores other aspects of the procedure that, although not necessary for completeness, are crucial for its effectiveness in practice. In this paper, we present a new calculus loosely based on FDPLL that lifts these aspects as well. In addition to being a more faithful litfing of the DPLL procedure, the new calculus contains a more systematic treatment ofuniversal literals, one of FDPLL's optimizations, and so has the potential of leading to much faster implementations.

Cesare Tinelli and Calogero Zarba.

Abstract.The Nelson-Oppen combination method combines decision procedures for first-order theories over disjoint signatures into a single decision procedure for the union theory. To be correct, the method requires that the component theories be stably infinite. This restriction makes the method inapplicable to many interesting theories such as, for instance, theories having only finite models. In this paper we provide a new combination method that can combine any theory that is not stably infinite with another theory, provided that the latter is what we call ashinytheory. Examples of shiny theories include the theory of equality, the theory of partial orders, and the theory of total orders. An interesting consequence of our results is that any decision procedure for the satisfiability of quantifier-free Σ-formulae in a Σ-theoryTcan always be extended to accept inputs over an arbitrary signature Ω ⊇ Σ.

Cesare Tinelli.

(Extended version of [Tin00].)

Abstract.We propose a general way of combining background reasoners in theory reasoning. Using a restricted version of the Craig Interpolation Lemma, we show that background reasoner cooperation can be achieved as a form of constraint propagation, much in the spirit of existing combination methods for decision procedures. In this case, constraint information is propagated across reasoners by exchangingresiduesthat are, in essence, disjunctions of ground literals over a common signature. As an application of our approach, we describe a multi-theory version of the semantic tableau calculus and we prove it sound and complete.

Franz Baader and Cesare Tinelli.

Abstract.This paper addresses the following combination problem: given two equational theories E_1 and E_2 whose positive theories are decidable, how can one obtain a decision procedure for the positive theory of E_1 U E_2? For theories over disjoint signatures, this problem was solved by Baader and Schulz in 1995. Our main new contribution is to extend this result to the case of theories sharing so-called constructors (and satisfying certain additional conditions). Since there is a close connection between positive theories and unification problems, this also extends to the non-disjoint case the work on combining decision procedures for unification modulo equational theories.

Cesare Tinelli and Christophe Ringeissen.

Abstract.In this paper we outline a theoretical framework for the combination of decision procedures for constraint satisfiability. We describe a general combination method which, given a procedure that decides constraint satisfiability with respect to a constraint theory T_1 and one that decides constraint satisfiability with respect to a constraint theory T_2, produces a procedure that (semi-)decides constraint satisfiability with respect to the union of T_1 and T_2. We provide a number of model-theoretic conditions on the constraint language and the component constraint theories for the method to be sound and complete, with special emphasis on the case in which the signatures of the component theories are non-disjoint. We also describe some general classes of theories to which our combination results apply, and relate our approach to some of the existing combination methods in the field.

Franz Baader and Cesare Tinelli.

Abstract.In a previous work, we describe a method to combine decision procedures for the word problem for theories sharing constructors. One of the requirements of our combination method is that the constructors becollapse-free. This paper removes that requirement by modifying the method so that it applies to non-collapse-free constructors as well. This broadens the scope of our combination results considerably, for example in the direction of equational theories corresponding to modal logics.

Franz Baader and Cesare Tinelli.

Abstract.The main contribution of this paper is a new method for combining decision procedures for the word problem in equational theories. In contrast to previous methods, it is based on transformation rules, and also applies to theories sharing ``constructors.'' In addition, we show that---contrary to a common belief---the Nelson-Oppen combination method cannot be used to combine decision procedures for the word problem, even in the case of equational theories with disjoint signatures.

Cesare Tinelli and Christophe Ringeissen.

Abstract.In this paper we outline a theoretical framework for the combination of decision procedures for the satisfiability of constraints with respect to a constraint theory. We describe a general combination method which, given a procedure that decides constraint satisfiability with respect to a constraint theory T_1 and one that decides constraint satisfiability with respect to a constraint theory T_2, is able to produce a procedure that (semi-)decides constraint satisfiability with respect to the union of T_1 and T_2. We also provide some model-theoretic conditions on the constraint language and the component constraint theories for the method to be sound and complete, with special emphasis on the case in which the signatures of T_1 and T_2 are non-disjoint.

Franz Baader and Cesare Tinelli.

Abstract.The Nelson-Oppen combination method can be used to combine decision procedures for the validity of quantifier-free formulae in first-order theories with disjoint signatures, provided that the theories to be combined are stably infinite. We show that, even though equational theories need not satisfy this property, Nelson and Oppen's method can be applied, after some minor modifications, to combine decision procedures for the validity of quantifier-free formulae in equational theories. Unfortunately, and contrary to a common belief, the method cannot be used to combine decision procedures for the word problem. We present a method that solves this kind of combination problem. Our method is based on transformation rules and also applies to equational theories that share a finite number of constant symbols.