{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T05:07:48Z","timestamp":1755925668440,"version":"3.40.3"},"reference-count":113,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,4,11]],"date-time":"2012-04-11T00:00:00Z","timestamp":1334102400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2012,7]]},"DOI":"10.1007\/s10601-012-9121-3","type":"journal-article","created":{"date-parts":[[2012,4,10]],"date-time":"2012-04-10T05:10:42Z","timestamp":1334034642000},"page":"304-347","source":"Crossref","is-referenced-by-count":46,"title":["An overview of parallel SAT solving"],"prefix":"10.1007","volume":"17","author":[{"given":"Ruben","family":"Martins","sequence":"first","affiliation":[]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,4,11]]},"reference":[{"key":"9121_CR1","doi-asserted-by":"crossref","unstructured":"Arbelaez, A., & Hamadi, Y. (2011). Improving parallel local search for SAT. In Learning and intelligent optimization (pp.\u00a046\u201360).","DOI":"10.1007\/978-3-642-25566-3_4"},{"issue":"2\u20133","key":"9121_CR2","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/AIC-2010-0462","volume":"23","author":"R As\u00edn","year":"2010","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., & Rodr\u00edguez-Carbonell, E. (2010). Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Communications, 23(2\u20133), 145\u2013157.","journal-title":"AI Communications"},{"key":"9121_CR3","doi-asserted-by":"crossref","unstructured":"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.\u00a021\u201327).","DOI":"10.1007\/978-3-540-79719-7_3"},{"key":"9121_CR4","unstructured":"Audemard, G., & Simon, L. (2009). Predicting learnt clauses quality in modern SAT solvers. In International joint conference on artificial intelligence (pp.\u00a0399\u2013404)."},{"key":"9121_CR5","unstructured":"Bacchus, F., & Winter, J. (2003). Effective preprocessing with hyper-resolution and equality reduction. In International conference on theory and applications of satisfiability testing (pp.\u00a0341\u2013355)."},{"key":"9121_CR6","doi-asserted-by":"crossref","unstructured":"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.\u00a0489\u2013494).","DOI":"10.1007\/3-540-45349-0_36"},{"key":"9121_CR7","unstructured":"Bayardo, R.\u00a0J., & Schrag, R.\u00a0C. (1997). Using CSP look-back techniques to solve real-world SAT instances. In AAAI conference on artificial intelligence (pp.\u00a0203\u2013208)."},{"issue":"2\u20134","key":"9121_CR8","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A. (2008). Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4(2\u20134), 75\u201397.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9121_CR9","unstructured":"Biere, A. (2009). PrecoSAT. SAT Competition, Solver Description."},{"key":"9121_CR10","unstructured":"Biere, A. (2010). Lingeling, plingeling, PicoSAT and PrecoSAT at SAT Race 2010. SAT Race, Solver Description."},{"key":"9121_CR11","unstructured":"Blochinger, W. (2005). Towards robustness in parallel SAT solving. In International conference on parallel computing (pp.\u00a0301\u2013308)."},{"issue":"7","key":"9121_CR12","doi-asserted-by":"crossref","first-page":"969","DOI":"10.1016\/S0167-8191(03)00068-1","volume":"29","author":"W Blochinger","year":"2003","unstructured":"Blochinger, W., Sinz, C., & K\u00fcchlin, W. (2003). Parallel propositional satisfiability checking with distributed dynamic learning. Journal of Parallel Computing, 29(7), 969\u2013994.","journal-title":"Journal of Parallel Computing"},{"key":"9121_CR13","doi-asserted-by":"crossref","unstructured":"Blochinger, W., Westje, W., Kuchlin, W., & Wedeniwski, S. (2005). ZetaSAT\u2014Boolean SATisfiability solving on desktop grids. In International symposium on cluster computing and the grid (pp.\u00a01079\u20131086).","DOI":"10.1109\/CCGRID.2005.1558680"},{"issue":"3\u20134","key":"9121_CR14","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M B\u00f6hm","year":"1996","unstructured":"B\u00f6hm, M., & Speckenmeyer, E. (1996). A fast parallel SAT-solver\u2014Efficient workload balancing. Annals of Mathematics and Artificial Intelligence, 17(3\u20134), 381\u2013400.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9121_CR15","unstructured":"Bordeaux, L., Hamadi, Y., & Samulowitz, H. (2009). Experiments with massively parallel constraint solving. In International joint conference on artificial intelligence (pp.\u00a0443\u2013448)."},{"key":"9121_CR16","doi-asserted-by":"crossref","unstructured":"Chrabakh, W., & Wolski, R. (2003). GridSAT: A Chaff-based distributed SAT solver for the grid. In International supercomputing conference (pp.\u00a037\u201349).","DOI":"10.1145\/1048935.1050188"},{"key":"9121_CR17","doi-asserted-by":"crossref","first-page":"99","DOI":"10.3233\/SAT190064","volume":"6","author":"G Chu","year":"2009","unstructured":"Chu, G., Harwood, A., & Stuckey. P.\u00a0J. (2009). Cache conscious data structures for Boolean satisfiability solvers. Journal on Satisfiability, Boolean Modeling and Computation, 6, 99\u2013120.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9121_CR18","doi-asserted-by":"crossref","unstructured":"Chu, G., Schulte, C., & Stuckey, P.\u00a0J. (2009). Confidence-based work stealing in parallel constraint programming. In International conference on principles and practice of constraint programming (pp.\u00a0226\u2013241).","DOI":"10.1007\/978-3-642-04244-7_20"},{"key":"9121_CR19","unstructured":"Chu, G., & Stuckey, P.\u00a0J. (2008). PMiniSAT : A parallelization of M iniSAT 2.0. SAT Race, Solver Description."},{"issue":"5035","key":"9121_CR20","doi-asserted-by":"crossref","first-page":"1181","DOI":"10.1126\/science.254.5035.1181","volume":"254","author":"SH Clearwater","year":"1991","unstructured":"Clearwater, S.\u00a0H., Huberman, B.\u00a0A., & Hogg, T. (1991). Cooperative solution of constraint satisfaction problems. Science, 254(5035), 1181\u20131183.","journal-title":"Science"},{"issue":"7","key":"9121_CR21","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5(7), 394\u2013397.","journal-title":"Communications of the ACM"},{"issue":"3","key":"9121_CR22","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM, 7(3), 201\u2013215.","journal-title":"Journal of the ACM"},{"key":"9121_CR23","doi-asserted-by":"crossref","unstructured":"Dequen, G., Vander-Swalmen, P., & Krajecki, M. (2009). Toward easy parallel SAT solving. In International conference on tools with artificial intelligence (pp.\u00a0425\u2013432).","DOI":"10.1109\/ICTAI.2009.63"},{"key":"9121_CR24","unstructured":"Edmund, M.\u00a0Y., Durfee, E.\u00a0H., Ishida, T., & Kuwabara, K. (1992). Distributed constraint satisfaction for formalizing distributed problem solving. In International conference on distributed computing systems (pp.\u00a0614\u2013621)."},{"key":"9121_CR25","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., & Biere, A. (2005). Effective preprocessing in SAT through variable and clause elimination. In International conference on theory and applications of satisfiability testing (pp.\u00a061\u201375).","DOI":"10.1007\/11499107_5"},{"key":"9121_CR26","unstructured":"E\u00e9n, N., & S\u00f6rensson, N. (2003). An extensible SAT-solver. In International conference on theory and applications of satisfiability testing (pp.\u00a0502\u2013518)."},{"key":"9121_CR27","doi-asserted-by":"crossref","unstructured":"Feldman, R., Monien, B., Mysliwietz, P., & Vornberger, O. (1990). Distributed game tree search. In Parallel algorithms for machine intelligence and pattern recognition (pp.\u00a066\u2013101). Springer-Verlag.","DOI":"10.1007\/978-1-4612-3390-9_3"},{"key":"9121_CR28","unstructured":"Feldmann, R., Monien, B., & Schamberger, S. (2000). A distributed algorithm to evaluate quantified Boolean formulae. In AAAI conference on artificial intelligence (pp.\u00a0285\u2013290)."},{"issue":"3","key":"9121_CR29","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.entcs.2004.10.020","volume":"128","author":"Y Feldman","year":"2005","unstructured":"Feldman, Y., Dershowitz, N., & Hanna, Z. (2005). Parallel multithreaded satisfiability solver: Design and implementation. Electronic Notes in Theoretical Computer Science, 128(3), 75\u201390.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9121_CR30","unstructured":"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.\u00a0236\u2013243)."},{"key":"9121_CR31","unstructured":"Gent, I.\u00a0P., Jefferson, C., Miguel, I., Moore, N.\u00a0C., Nightingale, P., Prosser, P., et al. (2011). A preliminary review of literature on parallel constraint solving. In Workshop on parallel methods for constraint solving."},{"key":"9121_CR32","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190063","volume":"6","author":"L Gil","year":"2008","unstructured":"Gil, L., Flores, P., & Silveira, L.\u00a0M. (2008). PMSat: A parallel version of MiniSAT. Journal on Satisfiability, Boolean Modeling and Computation, 6, 71\u201398.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9121_CR33","doi-asserted-by":"crossref","unstructured":"Goldberg, E. (2006). Determinization of resolution by an algorithm operating on complete assignments. In International conference on theory and applications of satisfiability testing (pp.\u00a090\u201395).","DOI":"10.1007\/11814948_11"},{"key":"9121_CR34","doi-asserted-by":"crossref","unstructured":"Goldberg, E. (2008). A decision-making procedure for resolution-based SAT-solvers. In International conference on theory and applications of satisfiability testing (pp.\u00a0119\u2013132).","DOI":"10.1007\/978-3-540-79719-7_11"},{"key":"9121_CR35","doi-asserted-by":"crossref","unstructured":"Goldberg, E., & Novikov, Y. (2002). BerkMin: A fast and robust SAT-solver. In Design, automation, and test in Europe (pp.\u00a0142\u2013149).","DOI":"10.1109\/DATE.2002.998262"},{"key":"9121_CR36","unstructured":"Gomes, C.\u00a0P., Selman, B., & Kautz, H. (1998). Boosting combinatorial search through randomization. In AAAI conference on artificial intelligence (pp.\u00a0431\u2013437)."},{"key":"9121_CR37","doi-asserted-by":"crossref","unstructured":"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.\u00a0252\u2013265).","DOI":"10.1007\/978-3-642-15396-9_22"},{"key":"9121_CR38","doi-asserted-by":"crossref","unstructured":"Hamadi, Y. (1999). Optimal distributed arc-consistency. In International conference on principles and practice of constraint programming (pp.\u00a0219\u2013233).","DOI":"10.1007\/978-3-540-48085-3_16"},{"issue":"2","key":"9121_CR39","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1142\/S0218213002000836","volume":"11","author":"Y Hamadi","year":"2002","unstructured":"Hamadi, Y. (2002). Interleaved backtracking in distributed constraint networks. International Journal on Artificial Intelligence Tools, 11(2), 167\u2013188.","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"9121_CR40","unstructured":"Hamadi, Y. (2003). Disolver: A distributed constraint solver. Technical Report MSR-TR-2003-91, Microsoft Research."},{"issue":"4","key":"9121_CR41","doi-asserted-by":"crossref","first-page":"127","DOI":"10.3233\/SAT190081","volume":"7","author":"Y Hamadi","year":"2011","unstructured":"Hamadi, Y., Jabbour, S., Piette, C., & Sais, L. (2011). Deterministic parallel DPLL. Journal on Satisfiability, Boolean Modeling and Computation, 7(4), 127\u2013132.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9121_CR42","unstructured":"Hamadi, Y., Jabbour, S., & Sais, L. (2009). Control-based clause sharing in parallel SAT solving. In International joint conference on artificial intelligence (pp.\u00a0499\u2013504)."},{"key":"9121_CR43","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3233\/SAT190070","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., & Sais, L. (2009). ManySAT: A parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 6, 245\u2013262.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9121_CR44","doi-asserted-by":"crossref","unstructured":"Hamadi, Y., Marques-Silva, J., & Wintersteiger, C.\u00a0M. (2011). Lazy decomposition for distributed decision procedures. In International workshop on parallel and distributed methods in verification (pp.\u00a043\u201354).","DOI":"10.4204\/EPTCS.72.5"},{"issue":"3","key":"9121_CR45","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s10732-010-9134-2","volume":"17","author":"Y Hamadi","year":"2011","unstructured":"Hamadi, Y., & Ringwelski, G. (2011). Boosting distributed constraint satisfaction. Journal of heuristics, 17(3), 251\u2013279.","journal-title":"Journal of Heuristics"},{"key":"9121_CR46","doi-asserted-by":"crossref","unstructured":"Han, H., & Somenzi, F. (2009). On-the-fly clause improvement. In International conference on theory and applications of satisfiability testing (pp.\u00a0209\u2013222).","DOI":"10.1007\/978-3-642-02777-2_21"},{"key":"9121_CR47","unstructured":"Hertel, P., Bacchus, F., Pitassi, T., & Gelder, A.\u00a0V. (2008). Clause learning can effectively p-simulate general propositional resolution. In AAAI conference on artificial intelligence (pp.\u00a0283\u2013290)."},{"key":"9121_CR48","doi-asserted-by":"crossref","unstructured":"Hyv\u00e4rinen, A., Junttila, T., & Niemel\u00e4, I. (2006). A distribution method for solving SAT in grids. In International conference on theory and applications of satisfiability testing (pp.\u00a0430\u2013435).","DOI":"10.1007\/11814948_39"},{"key":"9121_CR49","doi-asserted-by":"crossref","unstructured":"Jacobson, V. (1988). Congestion avoidance and control. In Special interest group on data communication (pp.\u00a0314\u2013329).","DOI":"10.1145\/52324.52356"},{"key":"9121_CR50","doi-asserted-by":"crossref","unstructured":"Jurkowiak, B., Li, C.\u00a0M., & Utard, G. (2001). Parallelizing satz using dynamic workload balancing. In International conference on theory and applications of satisfiability testing (pp.\u00a0205\u2013211).","DOI":"10.1016\/S1571-0653(04)00321-X"},{"key":"9121_CR51","unstructured":"Kalinnik, N., Schubert, T., \u00c1brah\u00e1m, E., Wimmer, R., & Becker, B. (2009). Picoso\u2014A parallel interval constraint solver. In International conference on parallel and distributed processing techniques and applications (pp. 473\u2013479)."},{"issue":"3","key":"9121_CR52","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0004-3702(90)90009-O","volume":"45","author":"S Kasif","year":"1990","unstructured":"Kasif, S. (1990). On the parallel complexity of discrete relaxation in constraint satisfaction networks. Journal of Artificial Intelligence, 45(3), 275\u2013286.","journal-title":"Journal of Artificial Intelligence"},{"key":"9121_CR53","doi-asserted-by":"crossref","unstructured":"Kottler, S. (2010). SAT solving with reference points. In international conference on theory and applications of satisfiability testing (pp.\u00a0143\u2013157).","DOI":"10.1007\/978-3-642-14186-7_13"},{"key":"9121_CR54","unstructured":"Kottler, S., & Kaufmann, M. (2011). SArTagnan\u2014A parallel portfolio SAT solver with lockless physical clause sharing. In Pragmatics of SAT workshop."},{"key":"9121_CR55","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/S0166-218X(00)00262-6","volume":"107","author":"O Kullmann","year":"2000","unstructured":"Kullmann, O. (2000). Investigations on autark assignments. Discrete Applied Mathematics, 107, 99\u2013137.","journal-title":"Discrete Applied Mathematics"},{"key":"9121_CR56","doi-asserted-by":"crossref","unstructured":"Kunz, W., & Pradhan, D.\u00a0K. (992). Recursive learning: An attractive alternative to the decision tree for test generation in digital circuits. In International test conference (pp.\u00a0816\u2013825).","DOI":"10.1109\/TEST.1992.527905"},{"key":"9121_CR57","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D Le Berre","year":"2010","unstructured":"Le\u00a0Berre, D., & Parrain, A. (2010). The sat4j library, release 2.2 system description. Journal on Satisfiability Boolean Modeling and Computation, 7, 59\u201364.","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"9121_CR58","doi-asserted-by":"crossref","unstructured":"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.\u00a0509\u2013523).","DOI":"10.1007\/978-3-642-02777-2_46"},{"key":"9121_CR59","doi-asserted-by":"crossref","unstructured":"Lewis, M., Schubert, T., & Becker, B. (2007). Multithreaded SAT solving. In Asia and south pacific design automation conference (pp.\u00a0926\u2013931).","DOI":"10.1109\/ASPDAC.2007.358108"},{"key":"9121_CR60","unstructured":"Lewis, M., Schubert, T., & Becker, B. (2009). QMiraXT\u2014A multithreaded QBF solver. In Methoden und beschreibungssprachen zur modellierung und verifikation von Schaltungen und systemen (pp.\u00a07\u201316)."},{"issue":"4","key":"9121_CR61","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M Luby","year":"1993","unstructured":"Luby, M., Sinclair, A., & Zuckerman, D. (1993). Optimal speedup of Las Vegas algorithms. Journal of Information Processing Letters, 47(4), 173\u2013180.","journal-title":"Journal of Information Processing Letters"},{"issue":"1\u20134","key":"9121_CR62","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/s10472-005-0425-5","volume":"43","author":"I Lynce","year":"2005","unstructured":"Lynce, I., & Marques-Silva, J. (2005). Efficient data structures for backtrack search SAT solvers. Annals of Mathematics and Artificial Intelligence, 43(1\u20134), 137\u2013152.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9121_CR63","unstructured":"Mailler, R., & Lesser, V. (2004). Solving distributed constraint optimization problems using cooperative mediation. In International conference on autonomous agents and multiagent systems (pp.\u00a0438\u2013445)."},{"key":"9121_CR64","unstructured":"Manthey, N. (2011). Parallel SAT solving\u2014Using more cores. In Pragmatics of SAT workshop."},{"key":"9121_CR65","doi-asserted-by":"crossref","unstructured":"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.\u00a0161\u2013167).","DOI":"10.1109\/HPCSIM.2009.5195312"},{"key":"9121_CR66","unstructured":"Marques-Silva, J., Lynce, I., & Malik, S. (2009). Conflict-driven clause learning SAT solvers. In Handbook of satisfiability (Vol.\u00a0185, pp. 131\u2013153). IOS Press."},{"key":"9121_CR67","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J Marques-Silva","year":"1999","unstructured":"Marques-Silva, J., & Sakallah, K.\u00a0A. (1999). GRASP\u2014A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48. 506\u2013521.","journal-title":"IEEE Transactions on Computers"},{"key":"9121_CR68","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V., & Lynce, I. (2010). Improving search space splitting for parallel SAT solving. In International conference on tools with artificial intelligence (pp.\u00a0336\u2013343).","DOI":"10.1109\/ICTAI.2010.56"},{"issue":"1\u20132","key":"9121_CR69","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.artint.2004.09.003","volume":"16","author":"PJ Modi","year":"2005","unstructured":"Modi, P.\u00a0J., Shen, W.\u00a0M., Tambe, M., & Yokoo, M. (2005). Adopt: Asynchronous distributed constraint optimization with quality guarantees. Journal of Artificial Intelligence, 16(1\u20132), 149\u2013180.","journal-title":"Journal of Artificial Intelligence"},{"key":"9121_CR70","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: Engineering an efficient SAT solver. In Design automation conference (pp.\u00a0530\u2013535).","DOI":"10.1145\/378239.379017"},{"key":"9121_CR71","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/S0167-6423(97)00012-9","volume":"30","author":"T Nguyen","year":"1998","unstructured":"Nguyen, T., & Deville, Y. (1998). A distributed arc-consistency algorithm. Science of Computer Programming, 30, 227\u2013250.","journal-title":"Science of Computer Programming"},{"key":"9121_CR72","doi-asserted-by":"crossref","unstructured":"Ohmura, K., & Ueda, K. (2009). c-SAT: A parallel SAT solver for clusters. In International conference on theory and applications of satisfiability testing (pp.\u00a0524\u2013537).","DOI":"10.1007\/978-3-642-02777-2_47"},{"key":"9121_CR73","unstructured":"Pham, D.\u00a0N., Gretton, C. (2009). gNovelty(v. 2). SAT Competition, Solver Description."},{"key":"9121_CR74","unstructured":"Piette, C., Hamadi, Y., & Lakhdar, S. (2008). Vivifying propositional clausal formulae. In European conference on artificial intelligence (pp.\u00a0525\u2013529)."},{"key":"9121_CR75","unstructured":"Pilarski, S., & Hu, G. (2002). SAT with partial clauses and back-leaps. In Design automation conference (pp.\u00a0743\u2013746)."},{"key":"9121_CR76","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., & Darwiche, A. (2007). A lightweight component caching scheme for satisfiability solvers. In International conference on theory and applications of satisfiability testing (pp.\u00a0294\u2013299).","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"9121_CR77","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., & Darwiche, A. (2011). On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175, 512\u2013525.","journal-title":"Artificial Intelligence"},{"key":"9121_CR78","unstructured":"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.\u00a0188\u2013194)."},{"key":"9121_CR79","unstructured":"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."},{"key":"9121_CR80","doi-asserted-by":"crossref","unstructured":"Prestwich, S.\u00a0D., & Lynce, I. (2006). Local search for unsatisfiability. In International conference on theory and applications of satisfiability testing (pp.\u00a0283\u2013296).","DOI":"10.1007\/11814948_28"},{"key":"9121_CR81","doi-asserted-by":"crossref","unstructured":"Rolf, C.\u00a0C., & Kuchcinski, K. (2008). Load-balancing methods for parallel and distributed constraint solving. In Interational conference on cluster computing (pp.\u00a0304\u2013309).","DOI":"10.1109\/CLUSTR.2008.4663786"},{"key":"9121_CR82","unstructured":"Rolf, C.\u00a0C., & 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.\u00a038\u201352)."},{"key":"9121_CR83","doi-asserted-by":"crossref","unstructured":"Roll, A. (2001). Criticality and parallelism in GSAT. In Workshop on theory and applications of satisfiability testing (pp.\u00a0150\u2013161).","DOI":"10.1016\/S1571-0653(04)00319-1"},{"key":"9121_CR84","unstructured":"Ryan, L. (2004). Efficient algorithms for clause-learning SAT solvers. Master\u2019s thesis, Simon Fraser University."},{"key":"9121_CR85","doi-asserted-by":"crossref","unstructured":"Schubert, T., Lewis, M., & Becker, B. (2005). PaMira\u2014A parallel SAT solver with knowledge sharing. In International workshop on microprocessor test and verification (pp.\u00a029\u201336).","DOI":"10.1109\/MTV.2005.17"},{"key":"9121_CR86","doi-asserted-by":"crossref","first-page":"203","DOI":"10.3233\/SAT190068","volume":"6","author":"T Schubert","year":"2009","unstructured":"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\u2013222.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"9121_CR87","unstructured":"Schubert, T., Lewis, M., & Becker, B. (2010). Antom\u2014Solver description. SAT Race, Solver Description."},{"key":"9121_CR88","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/s10723-010-9160-1","volume":"8","author":"S Schulz","year":"2010","unstructured":"Schulz, S., & Blochinger, W. (2010). Parallel SAT solving on peer-to-peer desktop grids. Journal of Grid Computing, 8, 443\u2013471.","journal-title":"Journal of Grid Computing"},{"key":"9121_CR89","unstructured":"Selman, B., Kautz, H.\u00a0A., & Cohen, B. (1996). Local search strategies for satisfiability testing. In Cliques, coloring, and satisfiability: Second DIMACS implementation challenge (Vol.\u00a026, pp. 521\u2013532). American Mathematical Society."},{"key":"9121_CR90","unstructured":"Selman, B., Levesque, H., & Mitchell, D. (1992). A new method for solving hard satisfiability problems. In AAAI conference on artificial intelligence (pp.\u00a0440\u2013446)."},{"key":"9121_CR91","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., & Stalmarck, G. (2000). A tutorial on Stalmarck\u2019s proof procedure for propositional logic. Formal Methods in System Design, 16, 23\u201358.","journal-title":"Formal Methods in System Design"},{"key":"9121_CR92","unstructured":"Silaghi, M.-C., Sam-haroud, D., & Faltings, B.\u00a0V. (2000). Asynchronous search with aggregations. In AAAI conference on artificial intelligence (pp.\u00a0917\u2013922)."},{"key":"9121_CR93","doi-asserted-by":"crossref","unstructured":"Singer, D. (2006). Parallel resolution of the satisfiability problem: A survey. In Parallel combinatorial optimization (pp.\u00a0123\u2013147). Wiley.","DOI":"10.1002\/9780470053928.ch5"},{"key":"9121_CR94","doi-asserted-by":"crossref","unstructured":"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.\u00a0249\u2013258).","DOI":"10.1007\/978-3-540-68111-3_27"},{"key":"9121_CR95","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/S1571-0653(04)00323-3","volume":"9","author":"C Sinz","year":"2001","unstructured":"Sinz, C., Blochinger, W., & K\u00fcchlin, W. (2001). PaSAT\u2014Parallel SAT-Checking with lemma exchange: Implementation and applications. Electronic Notes in Discrete Mathematics, 9, 205\u2013216.","journal-title":"Electronic Notes in Discrete Mathematics"},{"key":"9121_CR96","unstructured":"Snir, M., Otto, S., Huss-Lederman, S., Walker, D., & Dongarra, J. (1998). MPI-the complete reference. MIT Press."},{"key":"9121_CR97","unstructured":"Soos, M. (2010). CryptoMiniSat 2.5.0. SAT Race, Solver Description."},{"key":"9121_CR98","unstructured":"S\u00f6reasson, N., & E\u00e9e, N. (2008). MINISAT 2.1 and MINISAT+\u2009+ 1.0\u2014SAT race 2008 editions. SAt Race, Solver Description."},{"key":"9121_CR99","unstructured":"Sripriya, G., Bundy, A., & Smaill, A. (2009). Concurrent-distributed programming techniques for SAT using DPLL-stalmarck. In Workshop on parallel satisfiability solving (pp.\u00a0168\u2013175)."},{"key":"9121_CR100","unstructured":"Tsuyuzaki, K., Ohmura, K., & Ueda, K. (2009). Satake: Solver description. SAT Competition, Solver Description."},{"key":"9121_CR101","doi-asserted-by":"crossref","unstructured":"Valiant, L., & Vazirani, V. (1985). NP is as easy as detecting unique solutions. In Symposium on theory of computing (pp.\u00a0458\u2013463).","DOI":"10.1145\/22145.22196"},{"key":"9121_CR102","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1023\/A:1006143621319","volume":"23","author":"A Gelder Van","year":"1999","unstructured":"Van\u00a0Gelder, A. (1999). Autarky pruning in propositional model elimination reduces failure redundancy. Journal of Automated Reasoning, 23, 137\u2013193.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"9121_CR103","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/s10766-009-0097-6","volume":"37","author":"P Vander-Swalmen","year":"2009","unstructured":"Vander-Swalmen, P., Dequen, G., & Krajecki, M. (2009). A collaborative approach for multi-threaded SAT solving. International Journal of Parallel Programming, 37(3), 324\u2013342.","journal-title":"International Journal of Parallel Programming"},{"key":"9121_CR104","doi-asserted-by":"crossref","unstructured":"Vautard, J., Lallouet, A., & Hamadi, Y. (2010). A parallel solving algorithm for quantified constraints problems. In International conference on tools with artificial intelligence (pp.\u00a0271\u2013274).","DOI":"10.1109\/ICTAI.2010.46"},{"key":"9121_CR105","unstructured":"Williams, R., Gomes, C.\u00a0P., & Selman, B. (2003). Backdoors to typical case complexity. In International joint conference on artificial intelligence (pp.\u00a01173\u20131178)."},{"key":"9121_CR106","doi-asserted-by":"crossref","unstructured":"Wintersteiger, C.\u00a0M., Hamadi, Y., & de\u00a0Moura, L.\u00a0M. (2009). A concurrent portfolio approach to smt solving. In Computer aided verification (pp.\u00a0715\u2013720).","DOI":"10.1007\/978-3-642-02658-4_60"},{"key":"9121_CR107","doi-asserted-by":"crossref","first-page":"673","DOI":"10.1109\/69.729707","volume":"10","author":"M Yokoo","year":"1998","unstructured":"Yokoo, M., Durfee, E.\u00a0H., Ishida, T., & Kuwabara, K. (1998). The distributed constraint satisfaction problem: Formalization and algorithms. IEEE Transactions on Knowledge and Data Engineering, 10, 673\u2013685.","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"9121_CR108","doi-asserted-by":"crossref","unstructured":"Zhang, H. (1997). SATO: An efficient propositional prover. In International conference on automated deduction (pp.\u00a0272\u2013275).","DOI":"10.1007\/3-540-63104-6_28"},{"key":"9121_CR109","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H Zhang","year":"1996","unstructured":"Zhang, H., Bonacina, M.\u00a0P., Bonacina, M.\u00a0P., & Hsiang, J. (1996). PSATO: A distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation, 21, 543\u2013560.","journal-title":"Journal of Symbolic Computation"},{"key":"9121_CR110","doi-asserted-by":"crossref","unstructured":"Zhang, L. (2005). On subsumption removal and on-the-fly CNF simplification. In International conference on theory and applications of satisfiability testing (pp.\u00a0482\u2013489).","DOI":"10.1007\/11499107_42"},{"key":"9121_CR111","unstructured":"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.\u00a0279\u2013285)."},{"key":"9121_CR112","unstructured":"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.\u00a0287\u2013298)."},{"key":"9121_CR113","unstructured":"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.\u00a010880\u201310885)."}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-012-9121-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10601-012-9121-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-012-9121-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:11:45Z","timestamp":1742926305000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10601-012-9121-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,11]]},"references-count":113,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["9121"],"URL":"https:\/\/doi.org\/10.1007\/s10601-012-9121-3","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"type":"print","value":"1383-7133"},{"type":"electronic","value":"1572-9354"}],"subject":[],"published":{"date-parts":[[2012,4,11]]}}}