×

zbMATH — the first resource for mathematics

Parallelizing SMT solving: lazy decomposition and conciliation. (English) Zbl 1444.68169
Summary: Satisfiability Modulo Theories (SMT) is the satisfiability problem for first-order formulae with respect to background theories. SMT extends the propositional satisfiability by introducing various underlying theories. To improve the efficiency of SMT solving, many efforts have been made on low-level algorithms but they generally cannot leverage the capability of parallel hardware. We propose a high-level and flexible framework, namely lazy decomposition and conciliation (LDC), to parallelize solving for quantifier-free SMT problems. Overall, a SMT problem is firstly decomposed into subproblems, then local reasoning inside each subproblem is conciliated with the global reasoning over the shared symbols across subproblems in parallel. LDC can be built on any existing solver without tuning its internal implementation, and is flexible as it is applicable to various underlying theories. We instantiate LDC in the theory of equality with uninterpreted functions, and implement a parallel solver PZ3 based on Z3. Experiment results on the benchmarks from SMT-LIB as well as random problems show the potential of LDC, as (1) PZ3 generally outperforms Z3 in 4 out of 8 problem subcategories under various core configurations; (2) PZ3 usually achieves super-linear speed-up over Z3 on problems with sparse structures, which makes it possible to choose an appropriate solver from Z3 and PZ3 in advance according to the structure of input problem; (3) compared to PCVC4, a state-of-the-art portfolio-based parallel SMT solver, PZ3 achieves speed-up on a larger portion of problems and has better overall speed-up ratio.
MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68W10 Parallel algorithms in computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Memik, S. O.; Fallah, F., Accelerated SAT-based scheduling of control/data flow graphs, (20th International Conference on Computer Design, Proceedings, ICCD 2002, VLSI in Computers and Processors, Freiburg, Germany, 16-18 September 2002, (2002), IEEE Computer Society), 395
[2] Nam, G.; Sakallah, K. A.; Rutenbar, R. A., Satisfiability-based layout revisited: detailed routing of complex FPGAs via search-based Boolean SAT, (Kaptanoglu, S.; Trimberger, S., Proceedings of the 1999 ACM/SIGDA Seventh International Symposium on Field Programmable Gate Arrays, FPGA 1999, Monterey, CA, USA, February 21-23, 1999, (1999), ACM), 167-175
[3] Biere, A.; Cimatti, A.; Clarke, E. M.; Fujita, M.; Zhu, Y., Symbolic model checking using SAT procedures instead of bdds, (Irwin, M. J., Proceedings of the 36th Conference on Design Automation, New Orleans, LA, USA, June 21-25, 1999, (1999), ACM Press), 317-320
[4] Bryant, R. E.; German, S. M.; Velev, M. N., Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Trans. Comput. Log., 2, 93-134, (2001) · Zbl 1365.68317
[5] Cook, S. A., The complexity of theorem-proving procedures, (Harrison, M. A.; Banerji, R. B.; Ullman, J. D., Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Shaker Heights, Ohio, USA, May 3-5, 1971, (1971), ACM), 151-158 · Zbl 0363.68125
[6] Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient SAT solver, (Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, (2001), ACM), 530-535
[7] Eén, N.; Sörensson, N., An extensible SAT-solver, (Giunchiglia, E.; Tacchella, A., Theory and Applications of Satisfiability Testing, 6th International Conference, Selected Revised Papers, SAT 2003, Santa Margherita Ligure, Italy, May 5-8, 2003, Lect. Notes Comput. Sci., vol. 2919, (2003), Springer), 502-518 · Zbl 1204.68191
[8] Barrett, C. W.; Sebastiani, R.; Seshia, S. A.; Tinelli, C., Satisfiability modulo theories, (Handbook of Satisfiability, Front. Artif. Intell. Appl., vol. 185, (2009)), 825-885
[9] Lahiri, S. K.; Seshia, S. A., The UCLID decision procedure, (Computer Aided Verification, 16th International Conference, Proceedings, CAV 2004, July 13-17, 2004, (2004)), 475-478 · Zbl 1103.68628
[10] Ganesh, V.; Dill, D. L., A decision procedure for bit-vectors and arrays, (Damm, W.; Hermanns, H., Computer Aided Verification, 19th International Conference, Proceedings, CAV 2007, Berlin, Germany, July 3-7, 2007, Lect. Notes Comput. Sci., vol. 4590, (2007), Springer), 519-531 · Zbl 1135.68472
[11] Brummayer, R.; Biere, A., Boolector: an efficient SMT solver for bit-vectors and arrays, (Kowalewski, S.; Philippou, A., Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Proceedings, TACAS 2009, York, UK, March 22-29, 2009, Lect. Notes Comput. Sci., vol. 5505, (2009), Springer), 174-177
[12] de Moura, L. M.; Rueß, H., An experimental evaluation of ground decision procedures, (Computer Aided Verification, 16th International Conference, Proceedings, CAV 2004, Boston, MA, USA, July 13-17, 2004, (2004)), 162-174 · Zbl 1103.68645
[13] de Moura, L. M.; Bjørner, N., Z3: an efficient SMT solver, (Ramakrishnan, C. R.; Rehof, J., Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings, TACAS 2008, Budapest, Hungary, March 29-April 6, 2008, Lect. Notes Comput. Sci., vol. 4963, (2008), Springer), 337-340
[14] Dutertre, B.; de Moura, L., The yices SMT solver, (2006)
[15] Barrett, C.; Conway, C. L.; Deters, M.; Hadarean, L.; Jovanovic, D.; King, T.; Reynolds, A.; Tinelli, C., Cvc4, (Gopalakrishnan, G.; Qadeer, S., Computer Aided Verification - 23rd International Conference, Proceedings, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Lect. Notes Comput. Sci., vol. 6806, (2011), Springer), 171-177
[16] Cimatti, A.; Griggio, A.; Schaafsma, B. J.; Sebastiani, R., The mathsat5 SMT solver, (Piterman, N.; Smolka, S. A., Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proceedings, TACAS 2013, Rome, Italy, March 16-24, 2013, Lect. Notes Comput. Sci., vol. 7795, (2013), Springer), 93-107 · Zbl 1381.68153
[17] Huth, M.; Ryan, M., Logic in computer science: modeling and reasoning about systems, (2004), Cambridge University Press · Zbl 1073.68001
[18] Nelson, G.; Oppen, D. C., Fast decision procedures based on congruence closure, J. ACM, 27, 356-364, (1980) · Zbl 0441.68111
[19] Craig, W., Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. Symb. Log., 22, 250-268, (1957) · Zbl 0081.24402
[20] McMillan, K. L., Interpolation and SAT-based model checking, (Hunt, W. A.; Somenzi, F., Computer Aided Verification, 15th International Conference, Proceedings, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Lect. Notes Comput. Sci., vol. 2725, (2003), Springer), 1-13 · Zbl 1278.68184
[21] Kovács, L.; Voronkov, A., Interpolation and symbol elimination, (Schmidt, R. A., Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Proceedings, Montreal, Canada, August 2-7, 2009, Lect. Notes Comput. Sci., vol. 5663, (2009), Springer), 199-213 · Zbl 1250.68193
[22] McMillan, K. L., An interpolating theorem prover, Theor. Comput. Sci., 345, 101-121, (2005) · Zbl 1079.68092
[23] Fuchs, A.; Goel, A.; Grundy, J.; Krstic, S.; Tinelli, C., Ground interpolation for the theory of equality, Log. Methods Comput. Sci., 8, (2012) · Zbl 1239.03022
[24] Kapur, D.; Majumdar, R.; Zarba, C. G., Interpolation for data structures, (Young, M.; Devanbu, P. T., Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, Portland, Oregon, USA, November 5-11, 2006, (2006), ACM), 105-116
[25] Brillout, A.; Kroening, D.; Rümmer, P.; Wahl, T., An interpolating sequent calculus for quantifier-free Presburger arithmetic, J. Autom. Reason., 47, 341-367, (2011) · Zbl 1259.03043
[26] Brillout, A.; Kroening, D.; Rümmer, P.; Wahl, T., Program verification via Craig interpolation for Presburger arithmetic with arrays, (Aderhold, M.; Autexier, S.; Mantel, H., 6th International Verification Workshop, VERIFY-2010, Edinburgh, UK, July 20-21, 2010, EPiC Ser. Comput., vol. 3, (2010), EasyChair), 31-46
[27] Bruttomesso, R.; Ghilardi, S.; Ranise, S., Rewriting-based quantifier-free interpolation for a theory of arrays, (Schmidt-Schauß, M., Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, Novi Sad, Serbia, May 30-June 1, 2011, LIPIcs. Leibniz Int. Proc. Inform., vol. 10, (2011), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 171-186 · Zbl 1236.68179
[28] Cimatti, A.; Griggio, A.; Sebastiani, R., Efficient generation of Craig interpolants in satisfiability modulo theories, ACM Trans. Comput. Log., 12, 7:1-7:54, (2010) · Zbl 1351.68247
[29] McMillan, K. L., Interpolants from Z3 proofs, (Bjesse, P.; Slobodová, A., International Conference on Formal Methods in Computer-Aided Design, FMCAD ’11, Austin, TX, USA, October 30-November 02, 2011, (2011), FMCAD Inc.), 19-27
[30] Rybalchenko, A.; Sofronie-Stokkermans, V., Constraint solving for interpolation, J. Symb. Comput., 45, 1212-1233, (2010) · Zbl 1213.68389
[31] Yorsh, G.; Musuvathi, M., A combination method for generating interpolants, (Nieuwenhuis, R., Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Proceedings, Tallinn, Estonia, July 22-27, 2005, Lect. Notes Comput. Sci., vol. 3632, (2005), Springer), 353-368 · Zbl 1135.03331
[32] Bruttomesso, R.; Ghilardi, S.; Ranise, S., Quantifier-free interpolation in combinations of equality interpolating theories, ACM Trans. Comput. Log., 15, 5:1-5:34, (2014) · Zbl 1287.03068
[33] Wintersteiger, C. M.; Hamadi, Y.; de Moura, L. M., A concurrent portfolio approach to SMT solving, (Bouajjani, A.; Maler, O., Computer Aided Verification, 21st International Conference, Proceedings, CAV 2009, Grenoble, France, June 26-July 2, 2009, Lect. Notes Comput. Sci., vol. 5643, (2009), Springer), 715-720
[34] Rozanov, M.; Strichman, O., Generating minimum transitivity constraints in p-time for deciding equality logic, Electron. Notes Theor. Comput. Sci., 198, 3-17, (2008) · Zbl 1277.68146
[35] Slaney, J.; Fujita, M.; Stickel, M., Automated reasoning and exhaustive search: quasigroup existence problems, Comput. Math. Appl., 29, 115-132, (1995) · Zbl 0827.20083
[36] Ackermann, W., Solvable cases of the decision problem, Stud. Logic Found. Math., (1954), North-Holland Amsterdam · Zbl 0056.24505
[37] Déharbe, D.; Fontaine, P.; Merz, S.; Paleo, B. W., Exploiting symmetry in SMT problems, (Bjørner, N.; Sofronie-Stokkermans, V., Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings, Wroclaw, Poland, July 31-August 5, 2011, Lect. Notes Comput. Sci., vol. 6803, (2011), Springer), 222-236 · Zbl 1341.68187
[38] Hamadi, Y.; Jabbour, S.; Sais, L., Manysat: a parallel SAT solver, JSAT, 6, 245-262, (2009) · Zbl 1193.68227
[39] Zhang, H.; Bonacina, M. P.; Hsiang, J., PSATO: a distributed propositional prover and its application to quasigroup problems, J. Symb. Comput., 21, 543-560, (1996) · Zbl 0863.68013
[40] Biere, A., Lingeling, plingeling and treengeling entering the SAT competition 2013, (Proceedings of SAT Competition: Solver and Benchmark Descriptions, Dep. Comput. Sci. Ser. Publ. B, vol. B-2013-1, (2013), University of Helsinki), 51-52
[41] Hamadi, Y.; Jabbour, S.; Sais, L., Control-based clause sharing in parallel SAT solving, (Boutilier, C., Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, Pasadena, California, USA, July 11-17, 2009, (2009)), 499-504
[42] Manthey, N., Parallel SAT solving - using more cores, (2011), Technische Universität Dresden, Technical Report KRR Report 11-02
[43] Hamadi, Y.; Marques-Silva, J.; Wintersteiger, C. M., Lazy decomposition for distributed decision procedures, (Barnat, J.; Heljanko, K., Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2011, Snowbird, Utah, USA, July 14, 2011, EPTCS, vol. 72, (2011)), 43-54
[44] Bayless, S.; Val, C. G.; Ball, T.; Hoos, H. H.; Hu, A. J., Efficient modular SAT solving for IC3, (Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, (2013), IEEE), 149-156
[45] Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50, 752-794, (2003) · Zbl 1325.68145
[46] Das, S.; Dill, D. L., Successive approximation of abstract transition relations, (16th Annual IEEE Symposium on Logic in Computer Science, Proceedings, Boston, Massachusetts, USA, June 16-19, 2001, (2001), IEEE Computer Society), 51-58
[47] Henzinger, T. A.; Jhala, R.; Majumdar, R.; Sutre, G., Lazy abstraction, (Launchbury, J.; Mitchell, J. C., Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002, (2002), ACM), 58-70 · Zbl 1323.68374
[48] McMillan, K. L., Lazy abstraction with interpolants, (Ball, T.; Jones, R. B., Computer Aided Verification, 18th International Conference, Proceedings, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Lect. Notes Comput. Sci., vol. 4144, (2006), Springer), 123-136 · Zbl 1188.68196
[49] Boudou, J.; Paleo, B. W., Compression of propositional resolution proofs by lowering subproofs, (Galmiche, D.; Larchey-Wendling, D., Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, Proceedings, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Lect. Notes Comput. Sci., vol. 8123, (2013), Springer), 59-73 · Zbl 1401.68274
[50] Cotton, S., Two techniques for minimizing resolution proofs, (Strichman, O.; Szeider, S., Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, Proceedings, SAT 2010, Edinburgh, UK, July 11-14, 2010, Lect. Notes Comput. Sci., vol. 6175, (2010), Springer), 306-312 · Zbl 1306.68140
[51] Fellner, A.; Paleo, B. W., Greedy pebbling for proof space compression, Int. J. Softw. Tools Technol. Transf., (2017)
[52] Boudou, J.; Fellner, A.; Paleo, B. W., Skeptik: a proof compression system, (Demri, S.; Kapur, D.; Weidenbach, C., Automated Reasoning - 7th International Joint Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings, IJCAR 2014, Vienna, Austria, July 19-22, 2014, Lect. Notes Comput. Sci., vol. 8562, (2014), Springer), 374-380 · Zbl 06348251
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.