{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:44:52Z","timestamp":1725543892281},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540341413"},{"type":"electronic","value":"9783540341420"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11752578_46","type":"book-chapter","created":{"date-parts":[[2006,6,8]],"date-time":"2006-06-08T23:44:36Z","timestamp":1149810276000},"page":"380-388","source":"Crossref","is-referenced-by-count":3,"title":["Parallel Resolution of the Satisfiability Problem (SAT) with OpenMP and MPI"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Singer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Vagner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"46_CR1","unstructured":"Bennaceur, H.: The satisfiability problem regarded as a constraint satisfaction problem. In: Proc. of ECAI 1996, pp. 155\u2013159 (1996)"},{"key":"46_CR2","unstructured":"B\u00f6ehm, M., Speckenmeyer, E.: A fast Parallel Sat Solver - efficient work load balancing. In: Third Int. Symp. on AI and Maths. AIMSA, Fort Lauderdale, Florida USA (1994)"},{"key":"46_CR3","unstructured":"Blochinger, W., Sinz, C., K\u00fcchlin, W.: PaSAT-Parallel SAT-Checking with Lemma Exchange: Implementation and Applications. In: Proc. of SAT 2001 [21] (2001)"},{"issue":"7","key":"46_CR4","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1016\/S0167-8191(03)00068-1","volume":"29","author":"W. Blochinger","year":"2003","unstructured":"Blochinger, W., Sinz, C., K\u00fcchlin, W.: Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Computing\u00a029(7), 969\u2013994 (2003)","journal-title":"Parallel Computing"},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"Cook, S.A., Mitchell, D.G.: Finding Hard Instance of the Satisfiability Problem: a survey. In: DIMACS Series in Discrete Maths. and TCS., vol.\u00a035, pp. 1\u201317. AMS (1997)","DOI":"10.1090\/dimacs\/035\/01"},{"key":"46_CR6","doi-asserted-by":"crossref","unstructured":"Chrabakh, W., Wolski, R.: GridSAT: a Chaff-based Distributed SAT Solver for the Grid. In: Super Computing Conference, SC 2003, Phoenix Arizona, USA (2003)","DOI":"10.1145\/1048935.1050188"},{"key":"46_CR7","doi-asserted-by":"crossref","unstructured":"Chrabakh, W., Wolski, R.: Solving \u201dhard\u201d stisfiability problems using GridSAT (2004), http:\/\/www.cs.ucsb.edu\/~chrabakh\/papers\/gridsat-hp.pdf","DOI":"10.1145\/1048935.1050188"},{"key":"46_CR8","first-page":"65","volume-title":"Trends in Functional Programming","author":"M. Cope","year":"2000","unstructured":"Cope, M., Gent, I., Hammond, K.: Parallel Heuristic Search in Haskell. In: Gilmore, S. (ed.) Trends in Functional Programming, vol.\u00a02, pp. 65\u201373. Intellect Books, Bristol (2000)"},{"key":"46_CR9","doi-asserted-by":"crossref","unstructured":"Davis, M., Logeman, G., Loveland, D.: A machine program for Theorem Proving. CACM, 5(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"46_CR10","unstructured":"Feldman, Y., Derschowitz, N., Hanna, Z.: Parallel Multithreaded Satisfiability Solver: Design and Implementation. In: PDMC 2004 (2004)"},{"key":"46_CR11","unstructured":"G\u00e9nisson, R., J\u00e9gou, P.: Davis-Putnam were already checking forward. In: Proc. of ECAI 1996, pp. 180\u2013184 (1996)"},{"key":"46_CR12","volume-title":"SAT 2000, Highlights of Satisfiability Research in the Year 2000, Frontiers in AI and Applications","author":"I. Gent","year":"2000","unstructured":"Gent, I., van Maaren, H., Walsh, T.: SAT 2000, Highlights of Satisfiability Research in the Year 2000, Frontiers in AI and Applications, vol.\u00a063. Kluwer AC. Publ., Dordrecht (2000)"},{"key":"46_CR13","doi-asserted-by":"crossref","unstructured":"Gu, J., Purdom, P.W., Franco, J., Wah, B.W.: Algorithms for Satisfiability (SAT) problem: a Survey. In: DIMACS Series in Dicrete Maths. and TCS., vol.\u00a035, pp. 19\u2013152. AMS (1996)","DOI":"10.1090\/dimacs\/035\/02"},{"key":"46_CR14","unstructured":"Habbas, Z., Krajecki, M., Singer, D.: Parallel resolution of CSP with OpenMP. In: Proc. of the second European Workshop on OpenMP, EWOMP 2000, Edinburgh, Scotland, pp. 1\u20138 (2000)"},{"key":"46_CR15","unstructured":"Habbas, Z., Krajecki, M., Singer, D.: Shared memory implementation of CSP resolution. In: Proc. of HLPP 2001, Orl\u00e9ans, France (2001)"},{"key":"46_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48086-2_88","volume-title":"Parallel Processing and Applied Mathematics","author":"Z. Habbas","year":"2002","unstructured":"Habbas, Z., Krajecki, M., Singer, D.: The Langford\u2019s Problem: a Challenge for Parallel Resolution of CSP. In: Wyrzykowski, R., Dongarra, J., Paprzycki, M., Wa\u015bniewski, J. (eds.) PPAM 2001. LNCS, vol.\u00a02328, Springer, Heidelberg (2002)"},{"key":"46_CR17","unstructured":"Habbas, Z., Krajecki, M., Singer, D.: Parallelizing Combinatorial Search in Shared Memory. In: Proc. of the third European Workshop on OpenMP, EWOMP 2002, Roma, Italy (2002)"},{"key":"46_CR18","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. Special issue of ICPP-HPSECA01. Int. Jour. of Computational Science and Engineering (IJCSE) (to be published, 2005)","DOI":"10.1504\/IJCSE.2005.009703"},{"key":"46_CR19","doi-asserted-by":"crossref","unstructured":"Jurkowiak, B., Li, C.M., Utard, G.: Parallelizing Satz Using Dynamic Workload Balancing. In: Proc. of SAT 2001 [21] (2001)","DOI":"10.1016\/S1571-0653(04)00321-X"},{"key":"46_CR20","unstructured":"Jurkowiak, B.: Programmation Haute Performance pour la R\u00e9solution des probl\u00e8mes SAT et CSP, Th\u00e8se de l\u2019Universit\u00e9 de Picardie, Amiens (2004)"},{"key":"46_CR21","series-title":"Electronic Notes in Discrete Mathematics","volume-title":"Proc. of the Workshop on Theory and Applications of Satisfiability Testing, (SAT 2001)","author":"H. Kautz","year":"2001","unstructured":"Kautz, H., Selman, B.: Proc. of the Workshop on Theory and Applications of Satisfiability Testing (SAT 2001). Electronic Notes in Discrete Mathematics, vol.\u00a09. Elsevier Science Publishers, Amsterdam (2001), http:\/\/www.elsevier.nl\/gej-ng\/31\/29\/24\/42\/show\/Products\/notes\/cover.htt"},{"key":"46_CR22","first-page":"366","volume-title":"15th Int. Joint Conference on AI, IJCAI 1997","author":"C.M. Li","year":"1997","unstructured":"Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: 15th Int. Joint Conference on AI, IJCAI 1997, pp. 366\u2013371. Morgan Kaufmann Pub., Nagoya (1997)"},{"issue":"1-2","key":"46_CR23","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1023\/A:1006326723002","volume":"24","author":"F. Massacci","year":"2000","unstructured":"Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT-problem: Encoding and analysis of the U.S. Data Encryption Standard. Journal of Automated Reasoning\u00a024(1-2), 165\u2013203 (2000), http:\/\/www.dis.uniroma1.it\/~massacci\/papers\/","journal-title":"Journal of Automated Reasoning"},{"key":"46_CR24","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of the 39th. DAC, Las Vegas, USA (2001)","DOI":"10.1145\/378239.379017"},{"key":"46_CR25","unstructured":"OpenMP Architecture Review Board, OpenMP C and C++ Application Program Interface, http:\/\/www.openmp.org"},{"key":"46_CR26","unstructured":"SATLIB: http:\/\/www.intellektik.informatik.tu-darmstadt.de\/SATLIB\/"},{"key":"46_CR27","unstructured":"SATLive: http:\/\/www.satlive.org"},{"key":"46_CR28","doi-asserted-by":"crossref","unstructured":"Singer, D.: Parallel Resolution of the Satisfiability Problem: a Survey. In: Talbi, E.-G. (ed.) Parallel Combinatorial Optimization, Wiley and Sons (to appear)","DOI":"10.1002\/9780470053928.ch5"},{"key":"46_CR29","volume-title":"MPI: the complete reference","author":"M. Snir","year":"1996","unstructured":"Snir, M., Otto, S.W., Huss-Lederman, S., Walker, D.W., Dongarra, J.: MPI: the complete reference. The MIT Press, Cambridge (1996)"},{"key":"46_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-45349-0_32","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"T. Walsh","year":"2000","unstructured":"Walsh, T.: SAT versus CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 441\u2013456. Springer, Heidelberg (2000)"},{"key":"46_CR31","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H. Zang","year":"1996","unstructured":"Zang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its applications to Quasigroup problems. Journal of Symbolic Computation\u00a021, 543\u2013560 (1996)","journal-title":"Journal of Symbolic Computation"},{"key":"46_CR32","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"L. Zang","year":"2004","unstructured":"Zang, L., Malik, S.: Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Parallel Processing and Applied Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11752578_46.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:02:48Z","timestamp":1619492568000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11752578_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540341413","9783540341420"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/11752578_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}