{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,20]],"date-time":"2023-01-20T19:08:02Z","timestamp":1674241682228},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s10817-005-1970-7","type":"journal-article","created":{"date-parts":[[2005,4,20]],"date-time":"2005-04-20T17:42:35Z","timestamp":1114018955000},"page":"73-101","source":"Crossref","is-referenced-by-count":25,"title":["A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers"],"prefix":"10.1007","volume":"34","author":[{"given":"Bernard","family":"Jurkowiak","sequence":"first","affiliation":[]},{"given":"Chu Min","family":"Li","sequence":"additional","affiliation":[]},{"given":"Gil","family":"Utard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","unstructured":"B\u00f6hm, M. and Speckenmeyer, E.: A fast parallel SAT-solver with efficient workload balancing, in Third International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, 1994."},{"key":"CR2","unstructured":"Braunstein, A., Mezard, M. and Zecchina, R.: Survey propagation: An algorithm for satisfiablility, http:\/\/www.ictp.trieste.it\/~zecchina\/sp."},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Cook, S. A.: The complexity of theorem proving procedures, in 3rd ACM Symp. on Theory of Computing, 1971, pp. 151?158.","DOI":"10.1145\/800157.805047"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Cook, S. A.: A short proof of the pigeon hole principle using extended resolution, SIGACT News (1976), 28?32.","DOI":"10.1145\/1008335.1008338"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G. and Loveland, D.: A machine program for theorem proving, Comm. ACM (1962), 394?397.","DOI":"10.1145\/368273.368557"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Davis, M. and Putnam, H.: A computing procedure for quantification theory, J. ACM (1960), 201?215.","DOI":"10.1145\/321033.321034"},{"key":"CR7","unstructured":"Dubois, O. and Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-SAT formulae, in B. Nebel (ed.), Proceedings of IJCAI-01, 17th International Joint Conference on Artificial Intelligence, Vol. 1, Seattle, Washington, 2001, pp. 248?253."},{"key":"CR8","unstructured":"Dubois, O. and Dequen, G.: Renormalization as a function of clause lengths for solving random k-SAT formulae, in J. Franco (ed.), Proceedings of SAT?2002, 5th International Symposium on Theory and Applications of Satisfiability Testing, Cincinnati, Ohio, 2002, pp. 130?132, http:\/\/gauss.ececs.uc.edu\/Workshops\/SAT\/sat2002list.html."},{"key":"CR9","unstructured":"Freeman, J. W.: Improvement to propositional satisfiability search algorithms, Ph.D. thesis, Univ. of Pennsylvania, Philadelphia, http:\/\/www.intellektik.informatik.tu-darmstadt.de\/SATLIB\/biblio.html, 1995."},{"key":"CR10","unstructured":"Gelder, A. V. and Tsuji, Y. K.: Satisfiability testing with more reasoning and less guessing, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 26 (1996)."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Germain, C., N\u00e9ri, V., Fedak, G. and Cappello, F.: Xtremweb: Building an experimental platform for global computing, in R. Buyya and M. Baker (eds.), Grid 2000, 1st IEEE\/ACM International Workshop on Grid Computing, Bangalore, India, NCS 1971, Springer-Verlag, 2000.","DOI":"10.1007\/3-540-44444-0_9"},{"key":"CR12","unstructured":"Grama, Y. and Kumar, V.: A survey of parallel search algorithms for discrete optimization problems, personnal communication, http:\/\/citeseer.nj.nec.com\/et93survey.html, University of Minnesota, 1993."},{"key":"CR13","unstructured":"Guerra e Silva, L., Marques Silva, J. P., Silveira, L. M. and Sakallah, K. A.: Timing analysis using propositional satisfiability, in Proceedings of the ICECS, 5th IEEE International Conference on Electronics, Circuits and Systems, Lisbon, Portugal, IEEE, 1998."},{"key":"CR14","unstructured":"Hirsch, E. A. and Kojevnikov, A.: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination, Technical Report PDMI preprint 9\/2001, Steklov Inst. of Math. at St. Petersburg, 2001."},{"key":"CR15","unstructured":"http:\/\/sdg.lcs.mit.edu\/satsolvers\/psolver."},{"key":"CR16","unstructured":"http:\/\/www.laria.u-picardie.fr\/~cli\/englishpage.html."},{"key":"CR17","unstructured":"http:\/\/www.lri.fr\/~simon\/satex\/satex.php3."},{"key":"CR18","unstructured":"Hoos, H. H. and Sttzle, T.: SATLIB: An online resource for research on SAT, in I. P. Gent, H. v. Maaren and T. Walsh (eds.), SAT 2000, IOS Press, 2000, pp. 283?292. SATLIB is available online at www.satlib.org."},{"key":"CR19","series-title":"Electronic Notes in Discrete Mathematics","volume-title":"Proceedings of SAT?2001","author":"B. Jurkowiak","year":"2001","unstructured":"Jurkowiak, B., Li, C. M. and Utard, G.: Parallelizing Satz using dynamic workload balancing, in H. Kautz and B. Selman (eds.), Proceedings of SAT?2001, Electronic Notes in Discrete Mathematics 9, Elsevier Science Publishers, Boston, MA, 2001."},{"key":"CR20","unstructured":"Kautz, H. and Selman, B.: Unifying SAT-based and graph-based planning, in T. Dean (ed.), Proceedings of IJCAI?99, 16th International Joint Conference on Aritificial Intelligence, Vol. 1, 1999, pp. 318?325."},{"key":"CR21","unstructured":"Kautz, H. and Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search, in Proceedings of AAAI?96, 13th National Conference on Artificial Intelligence, Portland, Oregon, AAAI Press, 1996, pp. 1194?1201."},{"key":"CR22","series-title":"Electronic Notes in Discrete Mathematics","volume-title":"Proceedings of SAT?2001","author":"D. Berre Le","year":"2001","unstructured":"Le Berre, D.: Exploiting the real power of unit propagation lookahead, in H. Kautz and B. Selman (eds.), Proceedings of SAT?2001, Electronic Notes in Discrete Mathematics 9, Elsevier Science Publishers, Boston, 2001."},{"key":"CR23","unstructured":"Li, C. M.: Integrating equivalency reasoning into Davis?Putnam procedure, in Proceedings of AAAI?2000, 17th National Conference on Artificial Intelligence, Austin, Texas, AAAI Press, 2000, pp. 291?296."},{"key":"CR24","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/S0020-0190(99)00088-5","volume":"71","author":"C. M. Li","year":"1999","unstructured":"Li, C. M.: A constraint-based approach to narrow search trees for satisfiability, Inform. Process. Lett. 71 (1999), 75?80.","journal-title":"Inform. Process. Lett."},{"key":"CR25","unstructured":"Li, C. M. and Anbulagan: Heuristic based on unit propagation for satisfiability problems, in T. Dean and M. E. Pollack (eds.), Proceedings of IJCAI?97, 15th International Joint Conference on Aritificial Intelligence, Vol. 1, Nagoya, Japan, 1997, pp. 366?371."},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"Li, C. M. and Anbulagan: Look-ahead versus look-back for satisfiability problems, in Proceedings of CP-97, Third International Conference on Principles and Practice of Constraint Programming, Shloss Hagenberg, Austria, LNCS 1330, Springer-Verlag, 1997, pp. 342?356.","DOI":"10.1007\/BFb0017450"},{"key":"CR27","unstructured":"Mitchell, D., Selman, B. and Levesque, H.: Hard and easy distributions of SAT problems, in Proceedings of AAAI?92, 10th National Conference on Artificial Intelligence, San Jose, California, AAAI Press, 1992, pp. 459?465."},{"key":"CR28","series-title":"Electronic Notes in Discrete Mathematics","volume-title":"Proceedings of SAT?2001","author":"M. W. Moskewicz","year":"2001","unstructured":"Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L. and Malik, S.: Chaff: Engineering an efficient SAT solver, in H. Kautz and B. Selman (eds.), Proceedings of SAT?2001, Electronic Notes in Discrete Mathematics 9, Elsevier Science Publishers, Boston, MA, 2001."},{"key":"CR29","unstructured":"Selman, B., Kautz, H. and Cohen, B.: Noise strategies for improving local search, in Proceedings of AAAI-94, 12th National Conference on Artificial Intelligence, Seattle, Washington, AAAI Press, 1994, pp. 337?343."},{"key":"CR30","unstructured":"Selman, B., Kautz, H. and McAllester, D.: Ten challenges in propositional reasoning and search, in T. Dean and M. E. Pollack (eds.), Proceedings of IJCAI-97, 15th International Joint Conference on Aritificial Intelligence, Vol. 1, Nagoya, Japan, 1997, pp. 50?54."},{"key":"CR31","series-title":"Electronic Notes in Discrete Mathematics","volume-title":"Proceedings of SAT?2001","author":"C. Sinz","year":"2001","unstructured":"Sinz, C., Blochinger, W. and Kchlin, W.: Parallel SAT-checking with lemma exchange: Implementation and applications, in H. Kautz and B. Selman (eds.), Proceedings of SAT?2001, Electronic Notes in Discrete Mathematics 9, Elsevier Science Publishers, Boston, MA, 2001."},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"Velev, M. N.: Formal verification of VLIW microprocessors with speculative execution, in CAV ?00, 12th Conference on Computer-Aided Verification, Chicago, Illinois, LNCS 1855, Springer-Verlag, 2000, pp. 296?311.","DOI":"10.1007\/10722167_24"},{"key":"CR33","unstructured":"Zhang, H.: Specifying Latin squares in propositional logic, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1997, Chapter 6, pp. 1?30."},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"Zhang, H.: An efficient propositional prover, in Proceedings of CADE?97, 14th International Conference on Automated Deduction, Townsville, Australia, LNCS 1249, Springer-Verlag, 1997, pp. 272?275.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"CR35","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. P. and Hsiang, J.: PSATO: A distributed propositional prover and its applications to quasigroup problems, J. Symbolic Comput. 21 (1996), 543?560.","journal-title":"J. Symbolic Comput."},{"issue":"9","key":"CR36","doi-asserted-by":"crossref","first-page":"1327","DOI":"10.1109\/32.6176","volume":"14","author":"S. Zhou","year":"1988","unstructured":"Zhou, S.: A trace-driven simulation study of dynamic load balancing, IEEE Trans. on Software Engineering 14(9) (September 1988), 1327?1341.","journal-title":"IEEE Trans. on Software Engineering"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-1970-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-1970-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-1970-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T01:07:43Z","timestamp":1586221663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-1970-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["11970"],"URL":"http:\/\/dx.doi.org\/10.1007\/s10817-005-1970-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":["Artificial Intelligence","Computational Theory and Mathematics","Software"],"published":{"date-parts":[[2005,1]]}}}