Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. (English) Zbl 1192.68627
Summary: Most state-of-the-art approaches for Satisfiability Modulo Theories \((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}{\text{-}}solver)\). Often \(\mathcal{T}\) is the combination \(\mathcal{T}_1 \cup \mathcal{T}_2\) of two (or more) simpler theories \((SMT(\mathcal{T}_1 \cup \mathcal{T}_2))\), s.t. the specific \({\mathcal{T}_i}{\text{-}}solvers\) must be combined. Up to a few years ago, the standard approach to \(SMT(\mathcal{T}_1 \cup \mathcal{T}_2)\) was to integrate the SAT solver with one combined \(\mathcal{T}_1 \cup \mathcal{T}_2{\text{-}}solver\), obtained from two distinct \({\mathcal{T}_i}{\text{-}}solvers\) by means of evolutions of Nelson and Oppen’s (NO) combination procedure, in which the \({\mathcal{T}_i}{\text{-}}solvers\) deduce and exchange interface equalities. Nowadays many state-of-the-art SMT solvers use evolutions of a more recent \(SMT(\mathcal{T}_1 \cup \mathcal{T}_2)\) procedure called Delayed Theory Combination (DTC), in which each \({\mathcal{T}_i}{\text{-}}solver\) interacts directly and only with the SAT solver, in such a way that part or all of the (possibly very expensive) reasoning effort on interface equalities is delegated to the SAT solver itself.
In this paper we present a comparative analysis of DTC vs. NO for \(SMT(\mathcal{T}_1 \cup \mathcal{T}_2)\). On the one hand, we explain the advantages of DTC in exploiting the power of modern SAT solvers to reduce the search. On the other hand, we show that the extra amount of Boolean search required to the SAT solver can be controlled. In fact, we prove two novel theoretical results, for both convex and non-convex theories and for different deduction capabilities of the \({\mathcal{T}_i}{\text{-}}solvers\), which relate the amount of extra Boolean search required to the SAT solver by DTC with the number of deductions and case-splits required to the \({\mathcal{T}_i}{\text{-}}solvers\) by NO in order to perform the same tasks: (i) under the same hypotheses of deduction capabilities of the \({\mathcal{T}_i}{\text{-}}solvers\) required by NO, DTC causes no extra Boolean search; (ii) using \({\mathcal{T}_i}{\text{-}}solvers\) with limited or no deduction capabilities, the extra Boolean search required can be reduced down to a negligible amount by controlling the quality of the \(\mathcal{T}\)-conflict sets returned by the \({\mathcal{T}_i}{\text{-}}solvers\).
In this paper we present a comparative analysis of DTC vs. NO for \(SMT(\mathcal{T}_1 \cup \mathcal{T}_2)\). On the one hand, we explain the advantages of DTC in exploiting the power of modern SAT solvers to reduce the search. On the other hand, we show that the extra amount of Boolean search required to the SAT solver can be controlled. In fact, we prove two novel theoretical results, for both convex and non-convex theories and for different deduction capabilities of the \({\mathcal{T}_i}{\text{-}}solvers\), which relate the amount of extra Boolean search required to the SAT solver by DTC with the number of deductions and case-splits required to the \({\mathcal{T}_i}{\text{-}}solvers\) by NO in order to perform the same tasks: (i) under the same hypotheses of deduction capabilities of the \({\mathcal{T}_i}{\text{-}}solvers\) required by NO, DTC causes no extra Boolean search; (ii) using \({\mathcal{T}_i}{\text{-}}solvers\) with limited or no deduction capabilities, the extra Boolean search required can be reduced down to a negligible amount by controlling the quality of the \(\mathcal{T}\)-conflict sets returned by the \({\mathcal{T}_i}{\text{-}}solvers\).
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
References:
| [1] | Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: automatic theorem proving for predicate abstraction refinement. In: Proc. CAV’04. LNCS, vol. 3114. Springer, New York (2004) · Zbl 1103.68604 |
| [2] | Barrett, C., Berezin, S.: CVC Lite: a new implementation of the cooperating validity checker. In: Proceedings of the 16th International Conference on Computer Aided Verification (CAV ’04). LNCS, vol. 3114. Springer, New York (2004) · Zbl 1103.68605 |
| [3] | Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Proc. LPAR’06. LNAI, vol. 4246. Springer, New York (2006) · Zbl 1165.68480 |
| [4] | Barrett, C., Tinelli, C.: Cvc3. In: Proc. CAV’07. LNCS, vol. 4590. Springer, New York (2007) |
| [5] | Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak’s method for combining decision procedures. In: Frontiers of Combining Systems (FROCOS). Lecture Notes in Artificial Intelligence. Springer, Santa Margherita Ligure (2002) · Zbl 1057.68109 |
| [6] | Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Proc. of IJCAR’06. LNAI, no. 4130 (2006) · Zbl 1222.03011 |
| [7] | Bozzano, M., Bruttomesso, R., Cimatti, A., Franzen, A., Hanna, Z., Khasidashvili, Z., Palti, A., Sebastiani, R.: Encoding RTL constructs for MathSAT: a preliminary report. In: Proc. PDPAR’05. ENTCS, vol. 144. Elsevier, Amsterdam (2006) · Zbl 1272.68230 |
| [8] | Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Proc. TACAS’05. LNCS, vol. 3440. Springer, New York (2005) · Zbl 1087.68630 |
| [9] | Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient satisfiability modulo theories via delayed theory combination. In: Proc. CAV 2005. LNCS, vol. 3576. Springer, New York (2005) · Zbl 1081.68610 |
| [10] | Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient theory combination via boolean search. Inf. Comput. 204(10), 1493–1525 (2006) · Zbl 1137.68578 · doi:10.1016/j.ic.2005.05.011 |
| [11] | Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: Proc. ASP-DAC 2002, pp. 741–746. IEEE, Piscataway (2002) |
| [12] | Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. In: Proc. LPAR’06. LNAI, vol. 4246. Springer, New York (2006) · Zbl 1165.68483 |
| [13] | Bruttomesso, R., Cimatti, A., Franzen, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT solver. In: CAV. LNCS, vol. 5123. Springer, New York (2008) |
| [14] | Cotton, S., Maler, O.: Fast and flexible difference logic propagation for DPLL(T). In: Proc. SAT’06. LNCS, vol. 4121. Springer, New York (2006) · Zbl 1187.68537 |
| [15] | de Moura, L., Bjørner, N.: Model-based theory combination. In: Proc. of the 5th Workshop on Satisfiability Modulo Theories SMT’07. http://www.lsi.upc.edu/\(\sim\)oliveras/smt07/ (2007) · Zbl 1277.03007 |
| [16] | de Moura, L., Owre, S., Ruess, H., Rushby, J., Shankar, N.: The ICS decision procedures for embedded deduction. In: Proc. IJCAR’04. LNCS, vol. 3097, pp. 218–222. Springer, New York (2004) · Zbl 1126.68575 |
| [17] | Detlefs, D., Nelson, G., Saxe, J.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005) · Zbl 1323.68462 · doi:10.1145/1066100.1066102 |
| [18] | Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Proc. CAV’06. LNCS, vol. 4144. Springer, New York (2006) |
| [19] | Dutertre, B., de Moura, L.: System description: Yices 1.0. In: Proc. on 2nd SMT competition, SMT-COMP’06. yices.csl.sri.com/yices-smtcomp06.pdf (2006) |
| [20] | Enderton, H.: A Mathematical Introduction to Logic. Academic, London (1972) · Zbl 0298.02002 |
| [21] | Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Proc. CAV’2001 (2001) · Zbl 0996.68559 |
| [22] | Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Proc. CAV 2003. LNCS. Springer, New York (2003) · Zbl 1278.68259 |
| [23] | Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In: Proc. LPAR’04. LNCS, vol. 3452. Springer, New York (2004) · Zbl 1108.68384 |
| [24] | Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Proc. CAV’04. LNCS, vol. 3114, pp. 175–188. Springer, New York (2004) · Zbl 1103.68616 |
| [25] | Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3), 221–249 (2004) · Zbl 1069.03008 · doi:10.1007/s10817-004-6241-5 |
| [26] | Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. In: Proc. FroCos’05. LNCS, vol. 3717. Springer, New York (2005) · Zbl 1171.03306 |
| [27] | Krstic, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Proc. Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007. LNAI, vol. 4720. Springer, New York (2007) · Zbl 1148.68466 |
| [28] | Krstić, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: TACAS’07. LNCS, vol. 4424. Springer, New York (2007) · Zbl 1186.68297 |
| [29] | Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Proc. of 5th International Workshop on Frontiers of Combining Systems (FroCos ’05). LNCS, vol. 3717. Springer, New York (2005) · Zbl 1171.68715 |
| [30] | Nelson, C.G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245–257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079 |
| [31] | Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Proc. 10th LPAR. LNAI, no. 2850, pp. 77–89. Springer, New York (2003) · Zbl 1273.68326 |
| [32] | Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Proc. CAV’05. LNCS, vol. 3576. Springer, New York (2005) · Zbl 1081.68629 |
| [33] | Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comp. Sci. 12, 291–302 (1980) · Zbl 0437.03007 · doi:10.1016/0304-3975(80)90059-6 |
| [34] | Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Proc FroCos’05. LNCS, vol. 3717. Springer, New York (2005) · Zbl 1171.68439 |
| [35] | Rueß, H., Shankar, N.: Deconstructing Shostak. In: Proc. LICS ’01. IEEE Computer Society, Piscataway (2001) · Zbl 1045.03015 |
| [36] | Sebastiani, R.: Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation, JSAT. 3, 141–224 (2007) · Zbl 1145.68501 |
| [37] | Shankar, N., Rueß, H.: Combining Shostak theories. Invited paper for Floc’02/RTA’02 (2002) · Zbl 1045.03015 |
| [38] | Shostak, R.: A pratical decision procedure for arithmetic with function symbols. J. ACM 26(2), 51–360 (1979) · Zbl 0496.03003 · doi:10.1145/322123.322137 |
| [39] | Shostak, R.: Deciding combinations of theories. J. ACM 31, 1–12 (1984) · Zbl 0629.68089 · doi:10.1145/2422.322411 |
| [40] | Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson–Oppen combination procedure. In: Proc. Frontiers of Combining Systems, FroCoS’06. Applied Logic. Kluwer, Dordrecht (1996) · Zbl 0893.03001 |
| [41] | Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comp. Sci. 290(1), 291–353 (2003) · Zbl 1018.68033 · doi:10.1016/S0304-3975(01)00332-2 |
| [42] | Tinelli, C., Zarba, C.: Combining nonstably infinite theories. J. Autom. Reason. 34(3), 209–238 (2005) · Zbl 1108.03014 · doi:10.1007/s10817-005-5204-9 |
| [43] | Zarba, C.G.: A tableau calculus for combining non-disjoint theories. In: Proc. Tableaux’02. Lecture Notes in Computer Science, vol. 2381, pp. 315–329. Springer, New York (2002) · Zbl 1016.03011 |
| [44] | Zarba, C.G.: Combining sets with integers. In: FroCos’02. Lecture Notes in Computer Science, vol. 2309, pp. 103–116. Springer, New York (2002) · Zbl 1057.68682 |
| [45] | Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proc. ICCAD ’01. IEEE, Piscataway (2001) |
| [46] | Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Proc. CAV’02. LNCS, no. 2404, pp. 17–36. Springer, New York (2002) · Zbl 1010.68530 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
