DPLL(\(T\)) with exhaustive theory propagation and its application to difference logic.

*(English)*Zbl 1081.68629
Etessami, Kousha (ed.) et al., Computer aided verification. 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27231-3/pbk). Lecture Notes in Computer Science 3576, 321-334 (2005).

Summary: At CAV’04 we presented the DPLL(\(T\)) approach for satisfiability modulo theories \(T\) [H. Ganzinger, G. Hagen, C. Tinelli, and the authors, Lect. Notes Comput. Sci. 3114, 175–188 (2004; Zbl 1103.68616)]. It is based on a general DPLL(\(X)\) engine whose \(X\) can be instantiated with different theory solvers Solver\(_{T}\) for conjunctions of literals.

Here we go one important step further: we require Solver\(_{T}\) to be able to detect all input literals that are \(T\)-consequences of the partial model that is being explored by DPLL(\(X)\). Although at first sight this may seem too expensive, we show that for difference logic the benefits compensate by far the costs.

Here we describe and discuss this new version of DPLL(\(T)\), the DPLL(\(X)\) engine, and our Solver\(_{T}\) for difference logic. The resulting very simple DPLL(\(T)\) system importantly outperforms the existing techniques for this logic. Moreover, it has very good scaling properties: especially on the larger problems it gives improvements of orders of magnitude w.r.t. the existing state-of-the-art tools.

For the entire collection see [Zbl 1078.68004].

Here we go one important step further: we require Solver\(_{T}\) to be able to detect all input literals that are \(T\)-consequences of the partial model that is being explored by DPLL(\(X)\). Although at first sight this may seem too expensive, we show that for difference logic the benefits compensate by far the costs.

Here we describe and discuss this new version of DPLL(\(T)\), the DPLL(\(X)\) engine, and our Solver\(_{T}\) for difference logic. The resulting very simple DPLL(\(T)\) system importantly outperforms the existing techniques for this logic. Moreover, it has very good scaling properties: especially on the larger problems it gives improvements of orders of magnitude w.r.t. the existing state-of-the-art tools.

For the entire collection see [Zbl 1078.68004].