{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:51:13Z","timestamp":1764402673095},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243177"},{"type":"electronic","value":"9783319243184"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24318-4_12","type":"book-chapter","created":{"date-parts":[[2015,9,11]],"date-time":"2015-09-11T05:42:56Z","timestamp":1441950176000},"page":"156-172","source":"Crossref","is-referenced-by-count":43,"title":["HordeSat: A Massively Parallel Portfolio SAT Solver"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Balyo","sequence":"first","affiliation":[]},{"given":"Peter","family":"Sanders","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Sinz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,27]]},"reference":[{"key":"12_CR1","first-page":"399","volume":"9","author":"G Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. IJCAI 9, 399\u2013404 (2009)","journal-title":"IJCAI"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-319-09284-3_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"G Audemard","year":"2014","unstructured":"Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197\u2013205. Springer, Heidelberg (2014)"},{"key":"12_CR3","unstructured":"Belov, A., Diepold, D., Heule, M.J., J\u00e4rvisalo, M.: Sat competition (2014)"},{"key":"12_CR4","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Balint, A., Belov, A., Heule, M.J.H., J\u00e4rvisalo, M. (ed.), Proceedings of SAT Competition 2013, vol. B-2013-1 of Department of Computer Science Series of Publications B, pp. 51\u201352. University of Helsinki, 2013 (2013)"},{"key":"12_CR5","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T.: Conflict-driven clause learning sat solvers. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pp. 131\u2013153 (2009)"},{"key":"12_CR6","unstructured":"Blochinger, W., Westje, W., Kuchlin, W., Wedeniwski, S.: Zetasat-boolean satisfiability solving on desktop grids. In: IEEE International Symposium on Cluster Computing and the Grid, 2005. CCGrid 2005, vol. 2, pp. 1079\u20131086. IEEE (2005)"},{"issue":"7","key":"12_CR7","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/362686.362692","volume":"13","author":"BH Bloom","year":"1970","unstructured":"Bloom, B.H.: Space\/time trade-offs in hash coding with allowable errors. Communications of the ACM 13(7), 422\u2013426 (1970)","journal-title":"Communications of the ACM"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Chrabakh, W., Wolski, R.: Gradsat: A parallel sat solver for the grid. In: Proceedings of IEEE SC03 (2003)","DOI":"10.1145\/1048935.1050188"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Chrabakh, W., Wolski, R.: Gridsat: A chaff-based distributed sat solver for the grid. In: Proceedings of the 2003 ACM\/IEEE conference on Supercomputing, p. 37. ACM (2003)","DOI":"10.1145\/1048935.1050188"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"12_CR11","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.M.: Pmsat: a parallel version of minisat. Journal on Satisfiability, Boolean Modeling and Computation 6, 71\u201398 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"6","key":"12_CR12","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1016\/0167-8191(96)00024-5","volume":"22","author":"W Gropp","year":"1996","unstructured":"Gropp, W., Lusk, E., Doss, N., Skjellum, A.: A high-performance, portable implementation of the mpi message passing interface standard. Parallel computing 22(6), 789\u2013828 (1996)","journal-title":"Parallel computing"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-15396-9_22","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2010","author":"L Guo","year":"2010","unstructured":"Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 252\u2013265. Springer, Heidelberg (2010)"},{"key":"12_CR14","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3233\/SAT190070","volume":"6","author":"Y Hamadi","year":"2008","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel sat solver. Journal on Satisfiability, Boolean Modeling and Computation 6, 245\u2013262 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"12_CR15","unstructured":"H\u00f6lldobler, S., Manthey, N., Nguyen, V., Stecklina, J., Steinke, P.: A short overview on modern parallel sat-solvers. In: Proceedings of the International Conference on Advanced Computer Science and Information Systems, pp. 201\u2013206 (2011)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-642-23786-7_30","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"AEJ Hyv\u00e4rinen","year":"2011","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Grid-Based SAT solving with iterative partitioning and clause learning. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 385\u2013399. Springer, Heidelberg (2011)"},{"key":"12_CR17","doi-asserted-by":"crossref","first-page":"223","DOI":"10.3233\/SAT190069","volume":"6","author":"AE Hyv\u00e4rinen","year":"2014","unstructured":"Hyv\u00e4rinen, A.E., Junttila, T., Niemela, I.: Incorporating clause learning in grid-based randomized sat solving. Journal on Satisfiability, Boolean Modeling and Computation 6, 223\u2013244 (2014)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-31612-8_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"AEJ Hyv\u00e4rinen","year":"2012","unstructured":"Hyv\u00e4rinen, A.E.J., Manthey, N.: Designing scalable parallel SAT solvers. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 214\u2013227. Springer, Heidelberg (2012)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"issue":"1","key":"12_CR20","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10817-005-1970-7","volume":"34","author":"B Jurkowiak","year":"2005","unstructured":"Jurkowiak, B., Li, C.M., Utard, G.: A parallelization scheme based on work stealing for a class of sat solvers. Journal of Automated Reasoning 34(1), 73\u2013101 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR21","first-page":"359","volume":"92","author":"HA Kautz","year":"1992","unstructured":"Kautz, H.A., Selman, B., et al.: Planning as satisfiability. ECAI 92, 359\u2013363 (1992)","journal-title":"ECAI"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 21(12) (2002)","DOI":"10.1109\/TCAD.2002.804386"},{"issue":"5","key":"12_CR23","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"12_CR24","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/s10601-012-9121-3","volume":"17","author":"R Martins","year":"2012","unstructured":"Martins, R., Manquinho, V., Lynce, I.: An overview of parallel sat solving. Constraints 17(3), 304\u2013347 (2012)","journal-title":"Constraints"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/978-3-642-02777-2_47","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"K Ohmura","year":"2009","unstructured":"Ohmura, K., Ueda, K.: c-sat: a parallel SAT solver for clusters. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 524\u2013537. Springer, Heidelberg (2009)"},{"key":"12_CR27","unstructured":"Parkes, A.J.: Clustering at the phase transition. In: Proc. of the 14th Nat. Conf. on AI, pp. 340\u2013345. AAAI Press\/The MIT Press (1997)"},{"issue":"3","key":"12_CR28","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/s10723-010-9160-1","volume":"8","author":"S Schulz","year":"2010","unstructured":"Schulz, S., Blochinger, W.: Parallel sat solving on peer-to-peer desktop grids. Journal of Grid Computing 8(3), 443\u2013471 (2010)","journal-title":"Journal of Grid Computing"},{"key":"12_CR29","unstructured":"Sorensson, N., Een, N.: Minisat v1.13 a sat solver with conflict-clause minimization. SAT 2005 (2005)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Xu, L., Hoos, H., Leyton-Brown, K.: Hydra: Automatically configuring algorithms for portfolio-based selection. AAAI Conference on Artificial Intelligence (2010)","DOI":"10.1609\/aaai.v24i1.7565"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing -- SAT 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24318-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,13]],"date-time":"2023-08-13T23:49:43Z","timestamp":1691970583000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24318-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243177","9783319243184"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24318-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}