A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework

An increasing number of verification tools (e.g., soft-ware model-checkers) require the use of Satisfiability Modulo Theories (SMT) solvers to implement the back-ends for the automatic analysis of specifications and properties. The most prominent approach to build SMT solvers consists in integrating an efficient Boolean solver with decision procedures capable of checking the satisfia-bility of sets of ground literals in selected theories. Al-though the problem of checking the satisfiability of ar-bitrary Boolean combinations of atoms modulo a back-ground theory is NP-hard, there is a strong demand for high-performance SMT-solvers. In this paper, we describe the design and prototype im-plementation of—to the best of our knowledge—the first distributed SMT solver. The emphasis is on providing ways to reduce the implementation effort and to make the system easily extensible. This is achieved in two ways: (a) we re-use as much as possible the code of an available sequential SMT solver and (b) we adopt the TOOLBUS architecture for rapid prototyping. The behavior of the distributed SMT solver was tested on a set of problems which are representative of those generated by software verification techniques. The experiments show the possi-bility to obtain super-linear speed-ups of the distributed SMT solver with respect to its sequential version