{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T19:45:55Z","timestamp":1720640755816},"reference-count":24,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,6,1]],"date-time":"2001-06-01T00:00:00Z","timestamp":991353600000},"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":["Electronic Notes in Discrete Mathematics"],"published-print":{"date-parts":[[2001,6]]},"DOI":"10.1016\/s1571-0653(04)00321-x","type":"journal-article","created":{"date-parts":[[2005,4,9]],"date-time":"2005-04-09T09:34:04Z","timestamp":1113039244000},"page":"174-189","source":"Crossref","is-referenced-by-count":28,"special_numbering":"C","title":["Parallelizing Satz Using Dynamic Workload Balancing"],"prefix":"10.1016","volume":"9","author":[{"given":"Bernard","family":"Jurkowiak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chu Min","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gil","family":"Utard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0653(04)00321-X_BIB1","first-page":"203","article-title":"Using CSP Look-Back Techniques to Solve Real-World SAT Instances","author":"Bayardo","year":"1997","journal-title":"proceedings AAAI'97"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB2","first-page":"262","article-title":"Solving the round robin problem using prepositional logic","author":"B\u00e9jar","year":"2000","journal-title":"Proceedings of AAAP2000"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB3","series-title":"Third International Symposium on Artificial Intelligence and Mathematics","article-title":"A fast parallel SAT-solver - efficient workload balancing","author":"Boehm","year":"1994"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB4","first-page":"151","article-title":"The Complexity of Theorem Proving Procedures","author":"Cook","year":"1971","journal-title":"3rd ACM Symp. on Theory of Computing"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB5","doi-asserted-by":"crossref","DOI":"10.1016\/0004-3702(95)00046-1","article-title":"Experimental Results on the Crossover Point in random 3-SAT","volume":"81","author":"Crawford","year":"1996","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB6","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem proving","author":"Davis","year":"1962","journal-title":"Communication of ACM"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB7","series-title":"SAT versus UNSAT. Second DIMACS Challenge: Cliques, Coloring and Satisfiability","author":"Dubois","year":"1993"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB8","series-title":"Ph.d. thesis","article-title":"Improvement to Propositional Satisfiability Search Algorithms","author":"Freeman","year":"1995"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB9","article-title":"Towards an understanding of hill-climbing procedures for SAT","author":"Gent","year":"1993","journal-title":"proceedings AAAI-93"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB10","article-title":"Xtremweb: building an experimental platform for Global Computing","author":"Germain","year":"2000","journal-title":"Grid2000"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB11","series-title":"A Survey of Parallel Search Algorithms for Discrete Optimization Problems","author":"Grama","year":"1992"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB12","unstructured":"http:\/\/www.intellektik.informatik.tu-darmstadt.de\/satlib."},{"key":"10.1016\/S1571-0653(04)00321-X_BIB13","series-title":"Proceedings of AAAI'96","first-page":"4","article-title":"Pushing the envelope : Planing, prepositional logic, and stochastic search","author":"Kautz","year":"1996"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB14","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/S0020-0190(99)00088-5","article-title":"A constraint-based approach to narrow search trees for satisfiability","volume":"71","author":"Li","year":"1999","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB15","first-page":"366","article-title":"Heuristic based on unit propagation for satisfiability problems","author":"Li and Anbulagan","year":"1997","journal-title":"Proceedings IJCAI'97"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB16","article-title":"Conflict Analysis in Search Algorithms for Propositionnal Satisfiability","author":"Marques Silva","year":"1996","journal-title":"International Conference on Tools with Artificial Intelligence"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB17","article-title":"Tabu Search for SAT","author":"Mazure","year":"1997","journal-title":"proceedings AAAI'97"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB18","series-title":"proceedings AAAI'92","first-page":"459","article-title":"Hard and Easy Distributions of SAT Problems","author":"Mitchell","year":"1992"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB19","article-title":"Noise strategies for improving local search","author":"Selman","year":"1994","journal-title":"Proceedings AAAI-94"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB20","first-page":"50","article-title":"Ten Challenges in Prepositional Reasoning and Search","author":"Selman","year":"1997","journal-title":"proceedings IJCAI-97"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB21","first-page":"440","article-title":"A new Method for Solving Hard Satisfiability Problems","author":"Selman","year":"1992","journal-title":"proceedings AAAI'92"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB22","series-title":"Studies in constructive mathematics and mathematical logic, Part II (translated from Russian)","first-page":"115","article-title":"On the complexity of derivation in prepositional calculus","author":"Tseitin","year":"1970"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB23","first-page":"272","article-title":"An efficient prepositional prover","author":"Zhang","year":"1997","journal-title":"proceedings of int'Conf. on Automated Deduction"},{"key":"10.1016\/S1571-0653(04)00321-X_BIB24","doi-asserted-by":"crossref","DOI":"10.1006\/jsco.1996.0030","article-title":"PSATO: a Distributed Propositional Prover and Its Applications to Quasigroup Problems","author":"Zhang","year":"1996","journal-title":"J. Symbolic Computation"}],"container-title":["Electronic Notes in Discrete Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106530400321X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157106530400321X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,27]],"date-time":"2019-01-27T08:50:17Z","timestamp":1548579017000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157106530400321X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,6]]},"references-count":24,"alternative-id":["S157106530400321X"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0653(04)00321-x","relation":{},"ISSN":["1571-0653"],"issn-type":[{"value":"1571-0653","type":"print"}],"subject":[],"published":{"date-parts":[[2001,6]]}}}