Resumen de The dpll(t) approach to satisfiability y modulo theories
When solving a problem by means of automated theorem proving there are two important decisions to make: how to express and how to solve the problem, The choice of the logic in which to formalize the problem is usually based on the expressivity and the automation of the logic. Not surprisingly, the more expressive the logic the lower degree of automation it supports. Hence, one has to find the right balance between these two concepts. ver the last ten years, propositional logic has been shown to be very useful, due to its degree of automation, in areas such as electronic design automation, verification, artificial intelligence and operations research. Thanks to recent advances in the DPLL algorithm for propositional satisfiability (SAT), propositional solvers are becoming the tool of choice for attacking more and more practical problems. owever, for many applications encoding the problems into propositional logic is not the right choice. Frequently, a better alternative is to express the problems in a richer nonpropositional logic. This is why both the DPLL procedure and its enhancements have been adapted for handling satisfiability problems in more expressive logics. In particular, they have been used to build efficient algorithms for the Satisfiability Modulo Theories problem (SMT): deciding the satisfiability of ground first-order formulas with respect to background theories such as the integer or real numbers, the theory of equality, of arrays and so on. he topic of this thesis is the development of DPLL(T), a new approach to SMT. It is based on a general propositional engine DPLL(X), whose parameter X is instantiated with a solver for a theory T of interest thus giving a DPLL(T) system for deciding satisfiability of formulas modulo the theory T. he introduction of this approach is done by means of our Abstract DPLL framework. Apart from providing a simple and clean presentation of our approach, this framework also allows one to model the various existing techniq
