{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T22:40:09Z","timestamp":1684968009010},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,4,23]],"date-time":"2009-04-23T00:00:00Z","timestamp":1240444800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Parallel Prog"],"published-print":{"date-parts":[[2009,6]]},"DOI":"10.1007\/s10766-009-0097-6","type":"journal-article","created":{"date-parts":[[2009,4,22]],"date-time":"2009-04-22T08:51:37Z","timestamp":1240390297000},"page":"324-342","source":"Crossref","is-referenced-by-count":6,"title":["A Collaborative Approach for Multi-Threaded SAT Solving"],"prefix":"10.1007","volume":"37","author":[{"given":"Pascal","family":"Vander-Swalmen","sequence":"first","affiliation":[]},{"given":"Gilles","family":"Dequen","sequence":"additional","affiliation":[]},{"given":"Micha\u00ebl","family":"Krajecki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,4,23]]},"reference":[{"key":"97_CR1","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem proving procedures. In: 3rd ACM Symposium on Theory of Computing, pp. 151\u2013158. Ohio (1971)","DOI":"10.1145\/800157.805047"},{"issue":"2","key":"97_CR2","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1002\/rsa.20057","volume":"27","author":"A. Braunstein","year":"2005","unstructured":"Braunstein A., M\u00e9zard M., Zecchina R.: Survey propagation: an algorithm for satisfiability. Random Struct. Algorithms 27(2), 201\u2013226 (2005)","journal-title":"Random Struct. Algorithms"},{"key":"97_CR3","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: planning, propositional logic and stochastic search. In: Proceedings of the 30th National Conference on Artificial Intelligence and the 8th Innovative Applications of Artificial Intelligence Conference, pp. 1194\u20131201. AAAI Press \/ MIT Press, Menlo Park, 4\u20138 August 1996"},{"key":"97_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logic. Method Computer Sci. 2, (2006)","DOI":"10.2168\/LMCS-2(5:5)2006"},{"issue":"4","key":"97_CR5","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1109\/TVLSI.2007.893665","volume":"15","author":"N.R. Potlapally","year":"2007","unstructured":"Potlapally N.R., Raghunathan A., Ravi S., Jha N.K., Lee R.B.: Aiding side-channel attacks on cryptographic software with satisfiability-based analysis. IEEE Trans. VLSI Syst. 15(4), 465\u2013470 (2007)","journal-title":"IEEE Trans. VLSI Syst."},{"key":"97_CR6","first-page":"394","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis M., Logemann G., Loveland D.: A machine program for theorem-proving. J. Assoc. Comput. Mach. 5, 394\u2013397 (1962)","journal-title":"J. Assoc. Comput. Mach."},{"key":"97_CR7","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. (Online). Available: citeseer.ist.psu.edu\/bacchus03effective.html (2003)","DOI":"10.1007\/978-3-540-24605-3_26"},{"key":"97_CR8","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of ICCAD, San Jose, Nov 2001","DOI":"10.1145\/774572.774637"},{"key":"97_CR9","doi-asserted-by":"crossref","unstructured":"Habbas, Z., Krajecki, M., Singer, D.: Decomposition techniques for parallel resolution of constraint satisfaction problems in shared memory: a comparative study. Intern. J. Comput. Sci. Eng. (IJCSE). 1(2\/3\/4):192\u2013206, inderscience Publishers, ISSN : 1742\u20137185 (2005)","DOI":"10.1504\/IJCSE.2005.009703"},{"key":"97_CR10","doi-asserted-by":"crossref","unstructured":"Vander-Swalmen, P., Dequen, G., Krajecki, M.: On multi-threaded satisfiability solving with openmp. In: IWOMP, pp. 146\u2013157 (2008)","DOI":"10.1007\/978-3-540-79561-2_13"},{"key":"97_CR11","unstructured":"Hoos, H.H., St\u00fctzle, T.: Stochastic local search : foundations and applications (The Morgan Kaufmann Series in Artificial Intelligence). Morgan Kaufmann, September 2004"},{"issue":"4","key":"97_CR12","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10817-006-9025-2","volume":"37","author":"G. Dequen","year":"2006","unstructured":"Dequen G., Dubois O.: An efficient approach to solving random-satproblems. J. Autom. Reasoning. 37(4), 261\u2013276 (2006)","journal-title":"J. Autom. Reasoning."},{"issue":"4\u20136","key":"97_CR13","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., Hsiang J.: Psato: a distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21(4\u20136), 543\u2013560 (1996)","journal-title":"J. Symb. Comput."},{"key":"97_CR14","doi-asserted-by":"crossref","unstructured":"Jurkowiak, B., Li, C.M., Utard, G.: Parallelizing Satz using dynamic workload balancing. In: Proceedings of Workshop on Theory and Application of Satisfiability Testing (Sat\u20192001), pp. 205\u2013211. Boston, June 2001","DOI":"10.1016\/S1571-0653(04)00321-X"},{"key":"97_CR15","unstructured":"Mitchell, D., Selman, B., Levesque, H.J.: Hard and easy distribution of SAT problems. In: Proceedings of 10th National Conference on Artificial Intelligence, pp. 459\u2013465. AAAI (1992)"},{"issue":"2","key":"97_CR16","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/s10723-006-9042-8","volume":"4","author":"W. Chrabakh","year":"2006","unstructured":"Chrabakh W., Wolski R.: Gridsat: design and implementation of a computational grid application. J. Grid Comput. 4(2), 177\u2013193 (2006)","journal-title":"J. Grid Comput."},{"key":"97_CR17","unstructured":"Singer, D., Monnet, A.: JaCk-SAT: A new parallel scheme to solve the satisfiability problem (SAT) based on join-and-check. In: Proceedings of Parallel Processing and Applied Mathematics, Gdansk, (2007)"},{"key":"97_CR18","doi-asserted-by":"crossref","unstructured":"Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel multithreaded satisfiability solver: design and implementation (2004)","DOI":"10.1016\/j.entcs.2004.10.020"},{"key":"97_CR19","doi-asserted-by":"crossref","unstructured":"Lewis, M., Schubert, T., Becker, B.: Multithreaded sat solving. In: ASP-DAC \u201907: Proceedings of the 2007 Conference on Asia South Pacific Design Automation, pp. 926\u2013931. Washington, DC, USA: IEEE Computer Society (2007)","DOI":"10.1109\/ASPDAC.2007.358108"},{"key":"97_CR20","unstructured":"Silva, J.P.M., Sakallah, K.A.: Grasp a new search algorithm for satisfiability. In: ICCAD \u201996: Proceedings of the 1996 IEEE\/ACM International Conference on Computer-aided design, pp. 220\u2013227. Washington, DC, USA: IEEE Computer Society (1996)"},{"key":"97_CR21","unstructured":"Chu, G., Stuckey, P.J.: Pminisat: a parallelization of minisat 2.0. Tech. Rep. (Online). Available: http:\/\/www-sr.informatik.uni-tuebingen.de\/sat-race-2008\/descriptions\/solver_32.pdf (2008)"},{"key":"97_CR22","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Manysat a multicore sat solver (first rank at the sat race 2008 competition). Tech. Rep. (Online). Available: http:\/\/www-sr.informatik.uni-tuebingen.de\/sat-race-2008\/descriptions\/solver_24.pdf (2008)"},{"key":"97_CR23","unstructured":"Wand, Y.T., Morris, R.J.: Load sharing in distributed systems. IEEE Trans. Computers 202\u2013217 (1985)"},{"key":"97_CR24","unstructured":"Jaillet, C., Krajecki, M.: Parallel programming with openmp: a new memory allocation model avoiding cache faults. In: International Workshop on OpenMP 2007 (IWOMP2007). Tsinghua University, Beijing, China, jun 2007, short paper"}],"container-title":["International Journal of Parallel Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-009-0097-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10766-009-0097-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-009-0097-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T22:15:32Z","timestamp":1684966532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10766-009-0097-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4,23]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,6]]}},"alternative-id":["97"],"URL":"https:\/\/doi.org\/10.1007\/s10766-009-0097-6","relation":{},"ISSN":["0885-7458","1573-7640"],"issn-type":[{"value":"0885-7458","type":"print"},{"value":"1573-7640","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,4,23]]}}}