{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T04:28:16Z","timestamp":1726115296132},"reference-count":36,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Parallel Computing"],"published-print":{"date-parts":[[2003,7]]},"DOI":"10.1016\/s0167-8191(03)00068-1","type":"journal-article","created":{"date-parts":[[2003,6,2]],"date-time":"2003-06-02T23:25:49Z","timestamp":1054596349000},"page":"969-994","source":"Crossref","is-referenced-by-count":41,"title":["Parallel propositional satisfiability checking with distributed dynamic learning"],"prefix":"10.1016","volume":"29","author":[{"given":"Wolfgang","family":"Blochinger","sequence":"first","affiliation":[]},{"given":"Carsten","family":"Sinz","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0167-8191(03)00068-1_BIB1","series-title":"Proceedings of 6th International Workshop on High-Level Parallel Programming Models and Supportive Environments (HIPS \u201901) San Francisco","first-page":"55","article-title":"DSM-PM2: a portable implementation platform for multithreaded dsm consistency protocols","volume":"vol. 2026","author":"Antoniu","year":"2001"},{"issue":"3","key":"10.1016\/S0167-8191(03)00068-1_BIB2","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1145\/72551.72552","article-title":"Programming languages for distributed computing systems","volume":"21","author":"Bal","year":"1989","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB3","series-title":"Tools and Algorithms for the Analysis and Construction of Systems (TACAS\u201999)","article-title":"Symbolic model checking without BDDs","volume":"vol. 1579","author":"Biere","year":"1999"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB4","series-title":"Proceedings of International Parallel and Distributed Processing Symposium (10th Heterogeneous Computing Workshop) San Francisco, CA, USA","first-page":"90","article-title":"Distributed high performance computing in heterogeneous environments with DOTS","author":"Blochinger","year":"2001"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB5","series-title":"Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA 2000) Las Vegas, NV, USA, vol. 3","first-page":"1627","article-title":"Dependable high performance computing on a Parallel Sysplex cluster","author":"Blochinger","year":"2000"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB6","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/S0378-4754(99)00049-X","article-title":"An object-oriented platform for distributed high-performance symbolic computation","volume":"49","author":"Blochinger","year":"1999","journal-title":"Mathematics and Computers in Simulation"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB7","doi-asserted-by":"crossref","unstructured":"R.D. Blumofe, C.E. Leiserson, Scheduling multithreaded computations by work stealing, in: 35th Annual Symposium on Foundations of Computer Science (FOCS \u201994) Mexico, November 1994, pp. 356\u2013368","DOI":"10.1109\/SFCS.1994.365680"},{"issue":"3\u20134","key":"10.1016\/S0167-8191(03)00068-1_BIB8","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF02127976","article-title":"A fast parallel SAT-solver\u2013\u2013efficient workload balancing","volume":"17","author":"Boehm","year":"1996","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB9","series-title":"Proceedings of the Europar\u201997 Conference, Passau, Germany","first-page":"590","article-title":"Athapascan runtime: efficiency for irregular problems","author":"Briat","year":"1997"},{"issue":"1","key":"10.1016\/S0167-8191(03)00068-1_BIB10","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1006\/jpdc.1998.1434","article-title":"Solving large-scale QAP problems in parallel with the search library ZRAM","volume":"50","author":"Br\u00fcngger","year":"1998","journal-title":"Journal of Parallel and Distributed Computing"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB11","series-title":"Parallel Algorithms for Irregularly Structured Problems, IRREGULAR\u201995 Lyon, France","first-page":"231","article-title":"Distributed symbolic computation with DTS","volume":"vol. 980","author":"Bubeck","year":"1995"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB12","series-title":"3rd Symposium on Theory of Computing","first-page":"151","article-title":"The complexity of theorem proving procedures","author":"Cook","year":"1971"},{"issue":"7","key":"10.1016\/S0167-8191(03)00068-1_BIB13","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Communications of the ACM"},{"issue":"3","key":"10.1016\/S0167-8191(03)00068-1_BIB14","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"Journal of the ACM"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB15","doi-asserted-by":"crossref","first-page":"1825","DOI":"10.1016\/S0167-8191(00)00061-2","article-title":"Virtual data space\u2013\u2013load balancing for irregular applications","volume":"26","author":"Decker","year":"2000","journal-title":"Parallel Computing"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB16","unstructured":"Distributed Cilk. Available from <http:\/\/supertech.lcs.mit.edu\/cilk\/home\/distcilk5.1.html>"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB17","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1006\/jpdc.1996.0108","article-title":"The nexus approach to integrating multithreading and communication","volume":"37","author":"Foster","year":"1996","journal-title":"Journal of Parallel and Distributed Computing"},{"issue":"8","key":"10.1016\/S0167-8191(03)00068-1_BIB18","doi-asserted-by":"crossref","first-page":"929","DOI":"10.1002\/(SICI)1097-024X(199708)27:8<929::AID-SPE113>3.0.CO;2-#","article-title":"Millipede: easy parallel programming in available distributed environment","volume":"27","author":"Friedman","year":"1997","journal-title":"Software: Practice and Experience"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB19","series-title":"Proceedings of International Joint Conference on Artificial Intelligence IJCAI Chamb\u00e9ry, France","first-page":"52","article-title":"Automatic generation of some results in finite algebra","author":"Fujita","year":"1993"},{"issue":"1","key":"10.1016\/S0167-8191(03)00068-1_BIB20","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/69.755612","article-title":"State of the art in parallel search techniques for discrete optimization problems","volume":"11","author":"Grama","year":"1999","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB21","series-title":"Proceedings of the 1997 International Conference on Parallel and Distributed Systems (ICPADS\u201997) Seoul, Korea","first-page":"376","article-title":"Load balancing strategies for parallel forward search algorithm with conflict based backjumping","author":"Habbas","year":"1997"},{"issue":"3","key":"10.1016\/S0167-8191(03)00068-1_BIB22","doi-asserted-by":"crossref","first-page":"765","DOI":"10.1145\/174130.174145","article-title":"Randomized parallel algorithms for backtrack search and branch-and-bound computation","volume":"40","author":"Karp","year":"1993","journal-title":"Journal of the ACM"},{"issue":"129","key":"10.1016\/S0167-8191(03)00068-1_BIB23","doi-asserted-by":"crossref","first-page":"121","DOI":"10.2307\/2005469","article-title":"Estimating the efficiency of backtrack programs","volume":"29","author":"Knuth","year":"1975","journal-title":"Mathematics of Computation"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB24","unstructured":"J.P. Marques-Silva, K.A. Sakallah, Conflict analysis in search algorithms for propositional satisfiability, in: Proceedings of the IEEE International Conference on Tools with Artificial Intelligence, 1996"},{"issue":"1\u20132","key":"10.1016\/S0167-8191(03)00068-1_BIB25","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1023\/A:1006326723002","article-title":"Logical cryptanalysis as a SAT problem","volume":"24","author":"Massacci","year":"2000","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB26","series-title":"Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA \u201998) Las Vegas, NV, USA","article-title":"Parallel direct volume rendering on PC networks","author":"Meissner","year":"1998"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB27","series-title":"Proceedings of the 38th Design Automation Conference (DAC 2001)","first-page":"530","article-title":"Chaff: engineering an efficient SAT solver","author":"Moskewicz","year":"2001"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB28","unstructured":"F. Mueller, On the design and implementation of DSM-threads, in: International Conference on Parallel and Distributed Processing Techniques and Applications, 1997, pp. 315\u2013324"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB29","unstructured":"R. Namyst, PM2: an environment for a portable design and an efficient execution of irregular parallel applications, PhD thesis, Univ. de Lille 1, 1997 (in French)"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB30","unstructured":"K.H. Randall, Cilk: efficient multithreaded computing, PhD thesis, MIT Department of Electrical Engineering and Computer Science, 1998"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB31","unstructured":"T. R\u00fchl, H.E. Bal, G. Benson, R.A.F. Bhoedjang, K. Langendoen, Experience with a portability layer for implementing parallel programming systems, in: International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA\u201996) Sunnyvale, CA, 1996, pp. 1477\u20131488"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB32","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/280277.280278","article-title":"Models and languages for parallel computing","volume":"30","author":"Skillicorn","year":"1998","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB33","series-title":"Distributed Systems\u2013\u2013Principles and Paradigms","author":"Tanenbaum","year":"2002"},{"issue":"2","key":"10.1016\/S0167-8191(03)00068-1_BIB34","article-title":"Intelligent agents: theory and practice","volume":"10","author":"Woolridge","year":"1995","journal-title":"Knowledge Engineering Review"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB35","series-title":"Proceedings of 14th International Conference on Automated Deduction (CADE-97)","first-page":"272","article-title":"SATO: an efficient propositional prover","volume":"vol. 1249","author":"Zhang","year":"1997"},{"key":"10.1016\/S0167-8191(03)00068-1_BIB36","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1006\/jsco.1996.0030","article-title":"PSATO: a distributed propositional prover and its application to quasigroup problems","volume":"21","author":"Zhang","year":"1996","journal-title":"Journal of Symbolic Computation"}],"container-title":["Parallel Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167819103000681?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167819103000681?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,20]],"date-time":"2019-03-20T23:54:40Z","timestamp":1553126080000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167819103000681"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":36,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["S0167819103000681"],"URL":"https:\/\/doi.org\/10.1016\/s0167-8191(03)00068-1","relation":{},"ISSN":["0167-8191"],"issn-type":[{"value":"0167-8191","type":"print"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}