×

zbMATH — the first resource for mathematics

An overview of parallel SAT solving. (English) Zbl 1309.90057
Summary: Boolean satisfiability (SAT) solvers are currently very effective in practice. However, there are still many challenging problems for SAT solvers. Nowadays, extra computational power is no longer coming from higher processor frequencies. At the same time, multicore architectures are becoming predominant. Exploiting this new architecture is essential for the evolution of SAT solvers. Due to the increasing interest in parallel SAT solving, it is important to give an overview of what has been done so far. This paper presents an overview of parallel SAT solving and it is expected to be a valuable document for researchers in this field. This overview covers the main topics of parallel SAT solving, namely, different approaches and a variety of clause sharing strategies. Additionally, an evaluation of multicore SAT solvers is presented, showing the evolution of multicore SAT solvers over the last years.

MSC:
90C09 Boolean programming
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Arbelaez, A., & Hamadi, Y. (2011). Improving parallel local search for SAT. In Learning and intelligent optimization (pp. 46–60).
[2] Asín, R., Nieuwenhuis, R., Oliveras, A., & Rodríguez-Carbonell, E. (2010). Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Communications, 23(2–3), 145–157. · Zbl 1208.68195
[3] Audemard, G., Bordeaux, L., Hamadi, Y., Jabbour, S., & Sais, L. (2008). A generalized framework for conflict analysis. In International conference on theory and applications of satisfiability testing (pp. 21–27). · Zbl 1138.68485
[4] Audemard, G., & Simon, L. (2009). Predicting learnt clauses quality in modern SAT solvers. In International joint conference on artificial intelligence (pp. 399–404).
[5] Bacchus, F., & Winter, J. (2003). Effective preprocessing with hyper-resolution and equality reduction. In International conference on theory and applications of satisfiability testing (pp. 341–355). · Zbl 1204.68176
[6] Baptista, L., & Marques-Silva, J. (2000). Using randomization and learning to solve hard real-world instances of satisfiability. In International conference on principles and practice of constraint programming (pp. 489–494). · Zbl 1044.68736
[7] Bayardo, R. J., & Schrag, R. C. (1997). Using CSP look-back techniques to solve real-world SAT instances. In AAAI conference on artificial intelligence (pp. 203–208).
[8] Biere, A. (2008). Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4(2–4), 75–97. · Zbl 1159.68403
[9] Biere, A. (2009). PrecoSAT. SAT Competition, Solver Description.
[10] Biere, A. (2010). Lingeling, plingeling, PicoSAT and PrecoSAT at SAT Race 2010. SAT Race, Solver Description.
[11] Blochinger, W. (2005). Towards robustness in parallel SAT solving. In International conference on parallel computing (pp. 301–308).
[12] Blochinger, W., Sinz, C., & Küchlin, W. (2003). Parallel propositional satisfiability checking with distributed dynamic learning. Journal of Parallel Computing, 29(7), 969–994. · doi:10.1016/S0167-8191(03)00068-1
[13] Blochinger, W., Westje, W., Kuchlin, W., & Wedeniwski, S. (2005). ZetaSAT–Boolean SATisfiability solving on desktop grids. In International symposium on cluster computing and the grid (pp. 1079–1086).
[14] Böhm, M., & Speckenmeyer, E. (1996). A fast parallel SAT-solver–Efficient workload balancing. Annals of Mathematics and Artificial Intelligence, 17(3–4), 381–400. · Zbl 0891.68096 · doi:10.1007/BF02127976
[15] Bordeaux, L., Hamadi, Y., & Samulowitz, H. (2009). Experiments with massively parallel constraint solving. In International joint conference on artificial intelligence (pp. 443–448).
[16] Chrabakh, W., & Wolski, R. (2003). GridSAT: A Chaff-based distributed SAT solver for the grid. In International supercomputing conference (pp. 37–49).
[17] Chu, G., Harwood, A., & Stuckey. P. J. (2009). Cache conscious data structures for Boolean satisfiability solvers. Journal on Satisfiability, Boolean Modeling and Computation, 6, 99–120. · Zbl 1187.68169
[18] Chu, G., Schulte, C., & Stuckey, P. J. (2009). Confidence-based work stealing in parallel constraint programming. In International conference on principles and practice of constraint programming (pp. 226–241).
[19] Chu, G., & Stuckey, P. J. (2008). PMiniSAT : A parallelization of M iniSAT 2.0. SAT Race, Solver Description.
[20] Clearwater, S. H., Huberman, B. A., & Hogg, T. (1991). Cooperative solution of constraint satisfaction problems. Science, 254(5035), 1181–1183. · doi:10.1126/science.254.5035.1181
[21] Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5(7), 394–397. · Zbl 0217.54002 · doi:10.1145/368273.368557
[22] Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM, 7(3), 201–215. · Zbl 0212.34203 · doi:10.1145/321033.321034
[23] Dequen, G., Vander-Swalmen, P., & Krajecki, M. (2009). Toward easy parallel SAT solving. In International conference on tools with artificial intelligence (pp. 425–432). · Zbl 1191.68643
[24] Edmund, M. Y., Durfee, E. H., Ishida, T., & Kuwabara, K. (1992). Distributed constraint satisfaction for formalizing distributed problem solving. In International conference on distributed computing systems (pp. 614–621).
[25] Eén, N., & Biere, A. (2005). Effective preprocessing in SAT through variable and clause elimination. In International conference on theory and applications of satisfiability testing (pp. 61–75). · Zbl 1128.68463
[26] Eén, N., & Sörensson, N. (2003). An extensible SAT-solver. In International conference on theory and applications of satisfiability testing (pp. 502–518). · Zbl 1204.68191
[27] Feldman, R., Monien, B., Mysliwietz, P., & Vornberger, O. (1990). Distributed game tree search. In Parallel algorithms for machine intelligence and pattern recognition (pp. 66–101). Springer-Verlag.
[28] Feldmann, R., Monien, B., & Schamberger, S. (2000). A distributed algorithm to evaluate quantified Boolean formulae. In AAAI conference on artificial intelligence (pp. 285–290).
[29] Feldman, Y., Dershowitz, N., & Hanna, Z. (2005). Parallel multithreaded satisfiability solver: Design and implementation. Electronic Notes in Theoretical Computer Science, 128(3), 75–90. · doi:10.1016/j.entcs.2004.10.020
[30] Forman, S., & Segre, A. (2002). NAGSAT: A randomized, complete, parallel solver for 3-SAT. In International conference on theory and applications of satisfiability testing (pp. 236–243).
[31] Gent, I. P., Jefferson, C., Miguel, I., Moore, N. C., Nightingale, P., Prosser, P., et al. (2011). A preliminary review of literature on parallel constraint solving. In Workshop on parallel methods for constraint solving.
[32] Gil, L., Flores, P., & Silveira, L. M. (2008). PMSat: A parallel version of MiniSAT. Journal on Satisfiability, Boolean Modeling and Computation, 6, 71–98. · Zbl 1187.68542
[33] Goldberg, E. (2006). Determinization of resolution by an algorithm operating on complete assignments. In International conference on theory and applications of satisfiability testing (pp. 90–95). · Zbl 1187.68543
[34] Goldberg, E. (2008). A decision-making procedure for resolution-based SAT-solvers. In International conference on theory and applications of satisfiability testing (pp. 119–132). · Zbl 1138.68539
[35] Goldberg, E., & Novikov, Y. (2002). BerkMin: A fast and robust SAT-solver. In Design, automation, and test in Europe (pp. 142–149). · Zbl 1121.68106
[36] Gomes, C. P., Selman, B., & Kautz, H. (1998). Boosting combinatorial search through randomization. In AAAI conference on artificial intelligence (pp. 431–437).
[37] Guo, L., Hamadi, Y., Jabbour, S., & Sais, L. (2010). Diversification and intensification in parallel SAT solving. In International conference on principles and practice of constraint programming (pp. 252–265).
[38] Hamadi, Y. (1999). Optimal distributed arc-consistency. In International conference on principles and practice of constraint programming (pp. 219–233).
[39] Hamadi, Y. (2002). Interleaved backtracking in distributed constraint networks. International Journal on Artificial Intelligence Tools, 11(2), 167–188. · Zbl 05421354 · doi:10.1142/S0218213002000836
[40] Hamadi, Y. (2003). Disolver: A distributed constraint solver. Technical Report MSR-TR-2003-91, Microsoft Research.
[41] Hamadi, Y., Jabbour, S., Piette, C., & Sais, L. (2011). Deterministic parallel DPLL. Journal on Satisfiability, Boolean Modeling and Computation, 7(4), 127–132. · Zbl 1331.68208
[42] Hamadi, Y., Jabbour, S., & Sais, L. (2009). Control-based clause sharing in parallel SAT solving. In International joint conference on artificial intelligence (pp. 499–504). · Zbl 1193.68227
[43] Hamadi, Y., Jabbour, S., & Sais, L. (2009). ManySAT: A parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 6, 245–262. · Zbl 1193.68227
[44] Hamadi, Y., Marques-Silva, J., & Wintersteiger, C. M. (2011). Lazy decomposition for distributed decision procedures. In International workshop on parallel and distributed methods in verification (pp. 43–54).
[45] Hamadi, Y., & Ringwelski, G. (2011). Boosting distributed constraint satisfaction. Journal of heuristics, 17(3), 251–279. · Zbl 1153.68483 · doi:10.1007/s10732-010-9134-2
[46] Han, H., & Somenzi, F. (2009). On-the-fly clause improvement. In International conference on theory and applications of satisfiability testing (pp. 209–222).
[47] Hertel, P., Bacchus, F., Pitassi, T., & Gelder, A. V. (2008). Clause learning can effectively p-simulate general propositional resolution. In AAAI conference on artificial intelligence (pp. 283–290).
[48] Hyvärinen, A., Junttila, T., & Niemelä, I. (2006). A distribution method for solving SAT in grids. In International conference on theory and applications of satisfiability testing (pp. 430–435).
[49] Jacobson, V. (1988). Congestion avoidance and control. In Special interest group on data communication (pp. 314–329).
[50] Jurkowiak, B., Li, C. M., & Utard, G. (2001). Parallelizing satz using dynamic workload balancing. In International conference on theory and applications of satisfiability testing (pp. 205–211). · Zbl 0990.90546
[51] Kalinnik, N., Schubert, T., Ábrahám, E., Wimmer, R., & Becker, B. (2009). Picoso–A parallel interval constraint solver. In International conference on parallel and distributed processing techniques and applications (pp. 473–479).
[52] Kasif, S. (1990). On the parallel complexity of discrete relaxation in constraint satisfaction networks. Journal of Artificial Intelligence, 45(3), 275–286. · Zbl 0717.68043 · doi:10.1016/0004-3702(90)90009-O
[53] Kottler, S. (2010). SAT solving with reference points. In international conference on theory and applications of satisfiability testing (pp. 143–157). · Zbl 1306.68162
[54] Kottler, S., & Kaufmann, M. (2011). SArTagnan–A parallel portfolio SAT solver with lockless physical clause sharing. In Pragmatics of SAT workshop.
[55] Kullmann, O. (2000). Investigations on autark assignments. Discrete Applied Mathematics, 107, 99–137. · Zbl 0965.03018 · doi:10.1016/S0166-218X(00)00262-6
[56] Kunz, W., & Pradhan, D. K. (992). Recursive learning: An attractive alternative to the decision tree for test generation in digital circuits. In International test conference (pp. 816–825).
[57] Le Berre, D., & Parrain, A. (2010). The sat4j library, release 2.2 system description. Journal on Satisfiability Boolean Modeling and Computation, 7, 59–64.
[58] Lewis, M., Marin, P., Schubert, T., Narizzano, M., Becker, B., & Giunchiglia, E. (2009). PaQuBE: Distributed QBF solving with advanced knowledge sharing. In International conference on theory and applications of satisfiability testing (pp. 509–523).
[59] Lewis, M., Schubert, T., & Becker, B. (2007). Multithreaded SAT solving. In Asia and south pacific design automation conference (pp. 926–931).
[60] Lewis, M., Schubert, T., & Becker, B. (2009). QMiraXT–A multithreaded QBF solver. In Methoden und beschreibungssprachen zur modellierung und verifikation von Schaltungen und systemen (pp. 7–16).
[61] Luby, M., Sinclair, A., & Zuckerman, D. (1993). Optimal speedup of Las Vegas algorithms. Journal of Information Processing Letters, 47(4), 173–180. · Zbl 0797.68139 · doi:10.1016/0020-0190(93)90029-9
[62] Lynce, I., & Marques-Silva, J. (2005). Efficient data structures for backtrack search SAT solvers. Annals of Mathematics and Artificial Intelligence, 43(1–4), 137–152. · Zbl 1099.68025 · doi:10.1007/s10472-005-0425-5
[63] Mailler, R., & Lesser, V. (2004). Solving distributed constraint optimization problems using cooperative mediation. In International conference on autonomous agents and multiagent systems (pp. 438–445).
[64] Manthey, N. (2011). Parallel SAT solving–Using more cores. In Pragmatics of SAT workshop.
[65] Marin, P., Lewis, M., Schubert, T., Narizzano, M., Becker, B., & Giunchiglia, E. (2009). Comparison of knowledge sharing strategies in a parallel QBF solver. In Workshop on parallel satisfiability solving (pp. 161–167).
[66] Marques-Silva, J., Lynce, I., & Malik, S. (2009). Conflict-driven clause learning SAT solvers. In Handbook of satisfiability (Vol. 185, pp. 131–153). IOS Press.
[67] Marques-Silva, J., & Sakallah, K. A. (1999). GRASP–A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48. 506–521. · Zbl 01935259 · doi:10.1109/12.769433
[68] Martins, R., Manquinho, V., & Lynce, I. (2010). Improving search space splitting for parallel SAT solving. In International conference on tools with artificial intelligence (pp. 336–343). · Zbl 1306.68166
[69] Modi, P. J., Shen, W. M., Tambe, M., & Yokoo, M. (2005). Adopt: Asynchronous distributed constraint optimization with quality guarantees. Journal of Artificial Intelligence, 16(1–2), 149–180. · Zbl 1132.68706 · doi:10.1016/j.artint.2004.09.003
[70] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient SAT solver. In Design automation conference (pp. 530–535).
[71] Nguyen, T., & Deville, Y. (1998). A distributed arc-consistency algorithm. Science of Computer Programming, 30, 227–250. · Zbl 0895.68120 · doi:10.1016/S0167-6423(97)00012-9
[72] Ohmura, K., & Ueda, K. (2009). c-SAT: A parallel SAT solver for clusters. In International conference on theory and applications of satisfiability testing (pp. 524–537).
[73] Pham, D. N., Gretton, C. (2009). gNovelty(v. 2). SAT Competition, Solver Description.
[74] Piette, C., Hamadi, Y., & Lakhdar, S. (2008). Vivifying propositional clausal formulae. In European conference on artificial intelligence (pp. 525–529).
[75] Pilarski, S., & Hu, G. (2002). SAT with partial clauses and back-leaps. In Design automation conference (pp. 743–746).
[76] Pipatsrisawat, K., & Darwiche, A. (2007). A lightweight component caching scheme for satisfiability solvers. In International conference on theory and applications of satisfiability testing (pp. 294–299).
[77] Pipatsrisawat, K., & Darwiche, A. (2011). On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175, 512–525. · Zbl 1216.68235 · doi:10.1016/j.artint.2010.10.002
[78] Plaza, S., Kountanis, I., Andraus, Z., Bertacco, V., & Mudge, T. (2006). Advances and insights into parallel SAT solving. In International workshop on logic and synthesis (pp. 188–194).
[79] Plaza, S., Markov, I., & Bertacco, V. (2008). Low-latency SAT solving on multicore processors with priority scheduling and XOR partitioning. In International workshop on logic and synthesis.
[80] Prestwich, S. D., & Lynce, I. (2006). Local search for unsatisfiability. In International conference on theory and applications of satisfiability testing (pp. 283–296). · Zbl 1187.68561
[81] Rolf, C. C., & Kuchcinski, K. (2008). Load-balancing methods for parallel and distributed constraint solving. In Interational conference on cluster computing (pp. 304–309).
[82] Rolf, C. C., & Kuchcinski, K. (2010). Combining parallel search and parallel consistency in constraint programming. In TRICS workshop at the international conference on principles and practice of constraint programming (pp. 38–52).
[83] Roll, A. (2001). Criticality and parallelism in GSAT. In Workshop on theory and applications of satisfiability testing (pp. 150–161).
[84] Ryan, L. (2004). Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon Fraser University.
[85] Schubert, T., Lewis, M., & Becker, B. (2005). PaMira–A parallel SAT solver with knowledge sharing. In International workshop on microprocessor test and verification (pp. 29–36).
[86] Schubert, T., Lewis, M., & Becker, B. (2009). PaMiraXT: Parallel SAT solving with threads and message passing. Journal on Satisfiability, Boolean Modeling and Computation, 6, 203–222. · Zbl 1190.68057
[87] Schubert, T., Lewis, M., & Becker, B. (2010). Antom–Solver description. SAT Race, Solver Description.
[88] Schulz, S., & Blochinger, W. (2010). Parallel SAT solving on peer-to-peer desktop grids. Journal of Grid Computing, 8, 443–471. · Zbl 05785105 · doi:10.1007/s10723-010-9160-1
[89] Selman, B., Kautz, H. A., & Cohen, B. (1996). Local search strategies for satisfiability testing. In Cliques, coloring, and satisfiability: Second DIMACS implementation challenge (Vol. 26, pp. 521–532). American Mathematical Society. · Zbl 0864.90093
[90] Selman, B., Levesque, H., & Mitchell, D. (1992). A new method for solving hard satisfiability problems. In AAAI conference on artificial intelligence (pp. 440–446).
[91] Sheeran, M., & Stalmarck, G. (2000). A tutorial on Stalmarck’s proof procedure for propositional logic. Formal Methods in System Design, 16, 23–58. · doi:10.1023/A:1008725524946
[92] Silaghi, M.-C., Sam-haroud, D., & Faltings, B. V. (2000). Asynchronous search with aggregations. In AAAI conference on artificial intelligence (pp. 917–922).
[93] Singer, D. (2006). Parallel resolution of the satisfiability problem: A survey. In Parallel combinatorial optimization (pp. 123–147). Wiley.
[94] Singer, D., & Monnet, A. (2008). JaCk-SAT: A new parallel scheme to solve the satisfiability problem (SAT) based on join-and-check. In Parallel processing and applied mathematics (pp. 249–258).
[95] Sinz, C., Blochinger, W., & Küchlin, W. (2001). PaSAT–Parallel SAT-Checking with lemma exchange: Implementation and applications. Electronic Notes in Discrete Mathematics, 9, 205–216. · Zbl 0990.90563 · doi:10.1016/S1571-0653(04)00323-3
[96] Snir, M., Otto, S., Huss-Lederman, S., Walker, D., & Dongarra, J. (1998). MPI-the complete reference. MIT Press.
[97] Soos, M. (2010). CryptoMiniSat 2.5.0. SAT Race, Solver Description.
[98] Söreasson, N., & Eée, N. (2008). MINISAT 2.1 and MINISAT+ + 1.0–SAT race 2008 editions. SAt Race, Solver Description.
[99] Sripriya, G., Bundy, A., & Smaill, A. (2009). Concurrent-distributed programming techniques for SAT using DPLL-stalmarck. In Workshop on parallel satisfiability solving (pp. 168–175).
[100] Tsuyuzaki, K., Ohmura, K., & Ueda, K. (2009). Satake: Solver description. SAT Competition, Solver Description.
[101] Valiant, L., & Vazirani, V. (1985). NP is as easy as detecting unique solutions. In Symposium on theory of computing (pp. 458–463). · Zbl 0621.68030
[102] Van Gelder, A. (1999). Autarky pruning in propositional model elimination reduces failure redundancy. Journal of Automated Reasoning, 23, 137–193. · Zbl 0939.68108 · doi:10.1023/A:1006143621319
[103] Vander-Swalmen, P., Dequen, G., & Krajecki, M. (2009). A collaborative approach for multi-threaded SAT solving. International Journal of Parallel Programming, 37(3), 324–342. · Zbl 1191.68643 · doi:10.1007/s10766-009-0097-6
[104] Vautard, J., Lallouet, A., & Hamadi, Y. (2010). A parallel solving algorithm for quantified constraints problems. In International conference on tools with artificial intelligence (pp. 271–274).
[105] Williams, R., Gomes, C. P., & Selman, B. (2003). Backdoors to typical case complexity. In International joint conference on artificial intelligence (pp. 1173–1178).
[106] Wintersteiger, C. M., Hamadi, Y., & de Moura, L. M. (2009). A concurrent portfolio approach to smt solving. In Computer aided verification (pp. 715–720).
[107] Yokoo, M., Durfee, E. H., Ishida, T., & Kuwabara, K. (1998). The distributed constraint satisfaction problem: Formalization and algorithms. IEEE Transactions on Knowledge and Data Engineering, 10, 673–685. · Zbl 05109701 · doi:10.1109/69.729707
[108] Zhang, H. (1997). SATO: An efficient propositional prover. In International conference on automated deduction (pp. 272–275).
[109] Zhang, H., Bonacina, M. P., Bonacina, M. P., & Hsiang, J. (1996). PSATO: A distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation, 21, 543–560. · Zbl 0863.68013 · doi:10.1006/jsco.1996.0030
[110] Zhang, L. (2005). On subsumption removal and on-the-fly CNF simplification. In International conference on theory and applications of satisfiability testing (pp. 482–489). · Zbl 1128.68488
[111] Zhang, L., Madigan, C., Moskewicz, M., & Malik, S. (2001). Efficient conflict driven learning in a Boolean satisfiability solver. In International conference on computer-aided design (pp. 279–285).
[112] Zhang, L., & Malik, S. (2003). Cache performance of SAT solvers: A case study for efficient implementation of algorithms. In International conference on theory and applications of satisfiability testing (pp. 287–298). · Zbl 1204.68213
[113] Zhang, L., & Malik, S. (2003). Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Design, automation, and test in Europe (pp. 10880–10885).
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.