{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T05:55:20Z","timestamp":1725688520379},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642316111"},{"type":"electronic","value":"9783642316128"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31612-8_17","type":"book-chapter","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T05:14:42Z","timestamp":1339996482000},"page":"214-227","source":"Crossref","is-referenced-by-count":10,"title":["Designing Scalable Parallel SAT Solvers"],"prefix":"10.1007","author":[{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proc.\u00a0STOC 1971, pp. 151\u2013158. ACM (1971)","key":"17_CR1","DOI":"10.1145\/800157.805047"},{"unstructured":"B\u00e9jar, R., Many\u00e0, F.: Solving the round robin problem using propositional logic. In: Proc.\u00a0AAAI 2000, pp. 262\u2013266. AAAI Press\/MIT Press (2000)","key":"17_CR2"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT Solving for Termination Analysis with Polynomial Interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proc.\u00a0ECAI 1992, pp. 359\u2013363. John Wiley and Sons (1992)","key":"17_CR4"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/11814948_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"I. Lynce","year":"2006","unstructured":"Lynce, I., Marques-Silva, J.: SAT in Bioinformatics: Making the Case with Haplotype Inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 136\u2013141. Springer, Heidelberg (2006)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-16242-8_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A.E.J. Hyv\u00e4rinen","year":"2010","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Partitioning SAT Instances for Distributed Solving. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 372\u2013386. Springer, Heidelberg (2010)"},{"issue":"4","key":"17_CR7","doi-asserted-by":"publisher","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.: Optimal speedup of Las Vegas algorithms. Information Processing Letters\u00a047(4), 173\u2013180 (1993)","journal-title":"Information Processing Letters"},{"issue":"4","key":"17_CR8","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1109\/71.219757","volume":"4","author":"V.N. Rao","year":"1993","unstructured":"Rao, V.N., Kumar, V.: On the efficiency of parallel backtracking. IEEE Transactions on Parallel and Distributed Systems\u00a04(4), 427\u2013437 (1993)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-57785-8_163","volume-title":"STACS 94","author":"M. Luby","year":"1994","unstructured":"Luby, M., Ertel, W.: Optimal Parallelization of Las Vegas Algorithms. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol.\u00a0775, pp. 463\u2013474. Springer, Heidelberg (1994)"},{"issue":"1\/2","key":"17_CR10","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(02)00228-X","volume":"140","author":"A.M. Segre","year":"2002","unstructured":"Segre, A.M., Forman, S.L., Resta, G., Wildenberg, A.: Nagging: A scalable fault-tolerant paradigm for distributed search. Artificial Intelligence\u00a0140(1\/2), 71\u2013106 (2002)","journal-title":"Artificial Intelligence"},{"issue":"2-3","key":"17_CR11","doi-asserted-by":"crossref","first-page":"289","DOI":"10.3233\/FI-2011-404","volume":"107","author":"A.E.J. Hyv\u00e4rinen","year":"2011","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Partitioning search spaces of a randomized search. Fundamenta Informaticae\u00a0107(2-3), 289\u2013311 (2011)","journal-title":"Fundamenta Informaticae"},{"issue":"3-4","key":"17_CR12","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M. B\u00f6hm","year":"1996","unstructured":"B\u00f6hm, M., Speckenmeyer, E.: A fast parallel SAT-solver \u2014 efficient workload balancing. Annals of Mathematics and Artificial Intelligence\u00a017(3-4), 381\u2013400 (1996)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"Sinz, C., Blochinger, W., K\u00fcchlin, W.: PaSAT \u2014 parallel SAT-checking with lemma exchange: Implementation and applications. In: Proc.\u00a0SAT 2001. Electronic Notes in Discrete Mathematics, vol.\u00a09. Elsevier (2001)","key":"17_CR13","DOI":"10.1016\/S1571-0653(04)00323-3"},{"issue":"4","key":"17_CR14","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.: PaMiraXT: Parallel SAT solving with threads and message passing. Journal on Satisfiability, Boolean Modeling and Computation\u00a06(4), 203\u2013222 (2009)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"doi-asserted-by":"crossref","unstructured":"Heule, M.J., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In: Proc. HVC 2001. Springer (2011) (to appear)","key":"17_CR15","DOI":"10.1007\/978-3-642-34188-5_8"},{"issue":"5296","key":"17_CR16","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1126\/science.275.5296.51","volume":"275","author":"B.A. Huberman","year":"1997","unstructured":"Huberman, B.A., Lukose, R.M., Hogg, T.: An economics approach to hard computational problems. Science\u00a0275(5296), 51\u201354 (1997)","journal-title":"Science"},{"issue":"4","key":"17_CR17","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3233\/SAT190070","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sa\u00efs, L.: ManySAT: a parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation\u00a06(4), 245\u2013262 (2009)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"unstructured":"Hamadi, Y., Jabbour, S., Sa\u00efs, L.: Control-based clause sharing in parallel SAT solving. In: Proc.\u00a0IJCAI 2009, pp. 499\u2013504. IJCAI\/AAAI (2009)","key":"17_CR18"},{"key":"17_CR19","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.\u00a06308, pp. 252\u2013265. Springer, Heidelberg (2010)"},{"key":"17_CR20","doi-asserted-by":"crossref","first-page":"223","DOI":"10.3233\/SAT190069","volume":"6","author":"A.E.J. Hyv\u00e4rinen","year":"2009","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Incorporating clause learning in grid-based randomized SAT solving. Journal on Satisfiability, Boolean Modeling and Computation\u00a06, 223\u2013244 (2009)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/11814948_39","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"A.E.J. Hyv\u00e4rinen","year":"2006","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T.A., Niemel\u00e4, I.: A Distribution Method for Solving SAT in Grids. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 430\u2013435. Springer, Heidelberg (2006)"},{"key":"17_CR22","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":"A.E.J. 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.\u00a06876, pp. 385\u2013399. Springer, Heidelberg (2011)"},{"issue":"4-6","key":"17_CR23","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H. Zhang","year":"1996","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation\u00a021(4-6), 543\u2013560 (1996)","journal-title":"Journal of Symbolic Computation"},{"unstructured":"Hyv\u00e4rinen, A.E.J.: Grid Based Propositional Satisfiability Solving. PhD thesis, Aalto University (2011)","key":"17_CR24"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. DAC 2001, pp. 530\u2013535. ACM (2001)","key":"17_CR25","DOI":"10.1145\/378239.379017"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2012"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31612-8_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:40:10Z","timestamp":1620114010000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31612-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642316111","9783642316128"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31612-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}