Parallel Resolution of the Satisfiability Problem (SAT) with OpenMP and MPI

1. Bennaceur, H.: The satisfiability problem regarded as a constraint satisfaction problem. In: Proc. of ECAI 1996, pp. 155–159 (1996)

   Google Scholar 

2. Böehm, 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)

   Google Scholar 

3. Blochinger, W., Sinz, C., Küchlin, W.: PaSAT-Parallel SAT-Checking with Lemma Exchange: Implementation and Applications. In: Proc. of SAT 2001 [21] (2001)

   Google Scholar 

4. Blochinger, W., Sinz, C., Küchlin, W.: Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Computing 29(7), 969–994 (2003)

   Article  Google Scholar 

5. Cook, S.A., Mitchell, D.G.: Finding Hard Instance of the Satisfiability Problem: a survey. In: DIMACS Series in Discrete Maths. and TCS., vol. 35, pp. 1–17. AMS (1997)

   Google Scholar 

6. Chrabakh, W., Wolski, R.: GridSAT: a Chaff-based Distributed SAT Solver for the Grid. In: Super Computing Conference, SC 2003, Phoenix Arizona, USA (2003)

   Google Scholar 

7. Chrabakh, W., Wolski, R.: Solving ”hard” stisfiability problems using GridSAT (2004), http://www.cs.ucsb.edu/~chrabakh/papers/gridsat-hp.pdf

8. Cope, M., Gent, I., Hammond, K.: Parallel Heuristic Search in Haskell. In: Gilmore, S. (ed.) Trends in Functional Programming, vol. 2, pp. 65–73. Intellect Books, Bristol (2000)

   Google Scholar 

9. Davis, M., Logeman, G., Loveland, D.: A machine program for Theorem Proving. CACM, 5(7) (1962)

   Google Scholar 

10. Feldman, Y., Derschowitz, N., Hanna, Z.: Parallel Multithreaded Satisfiability Solver: Design and Implementation. In: PDMC 2004 (2004)

    Google Scholar 

11. Génisson, R., Jégou, P.: Davis-Putnam were already checking forward. In: Proc. of ECAI 1996, pp. 180–184 (1996)

    Google Scholar 

12. Gent, I., van Maaren, H., Walsh, T.: SAT 2000, Highlights of Satisfiability Research in the Year 2000, Frontiers in AI and Applications, vol. 63. Kluwer AC. Publ., Dordrecht (2000)

    MATH  Google Scholar 

13. 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. 35, pp. 19–152. AMS (1996)

    Google Scholar 

14. 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–8 (2000)

    Google Scholar 

15. Habbas, Z., Krajecki, M., Singer, D.: Shared memory implementation of CSP resolution. In: Proc. of HLPP 2001, Orléans, France (2001)

    Google Scholar 

16. Habbas, Z., Krajecki, M., Singer, D.: The Langford’s Problem: a Challenge for Parallel Resolution of CSP. In: Wyrzykowski, R., Dongarra, J., Paprzycki, M., Waśniewski, J. (eds.) PPAM 2001. LNCS, vol. 2328, Springer, Heidelberg (2002)

    Chapter  Google Scholar 

17. 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)

    Google Scholar 

18. 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)

    Google Scholar 

19. Jurkowiak, B., Li, C.M., Utard, G.: Parallelizing Satz Using Dynamic Workload Balancing. In: Proc. of SAT 2001 [21] (2001)

    Google Scholar 

20. Jurkowiak, B.: Programmation Haute Performance pour la Résolution des problèmes SAT et CSP, Thèse de l’Université de Picardie, Amiens (2004)

    Google Scholar 

21. Kautz, H., Selman, B.: Proc. of the Workshop on Theory and Applications of Satisfiability Testing (SAT 2001). Electronic Notes in Discrete Mathematics, vol. 9. Elsevier Science Publishers, Amsterdam (2001), http://www.elsevier.nl/gej-ng/31/29/24/42/show/Products/notes/cover.htt

    MATH  Google Scholar 

22. Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: 15th Int. Joint Conference on AI, IJCAI 1997, pp. 366–371. Morgan Kaufmann Pub., Nagoya (1997)

    Google Scholar 

23. Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT-problem: Encoding and analysis of the U.S. Data Encryption Standard. Journal of Automated Reasoning 24(1-2), 165–203 (2000), http://www.dis.uniroma1.it/~massacci/papers/

    Article  MathSciNet  MATH  Google Scholar 

24. 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)

    Google Scholar 

25. OpenMP Architecture Review Board, OpenMP C and C++ Application Program Interface, http://www.openmp.org

26. SATLIB: http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/

27. SATLive: http://www.satlive.org

28. Singer, D.: Parallel Resolution of the Satisfiability Problem: a Survey. In: Talbi, E.-G. (ed.) Parallel Combinatorial Optimization, Wiley and Sons (to appear)

    Google Scholar 

29. Snir, M., Otto, S.W., Huss-Lederman, S., Walker, D.W., Dongarra, J.: MPI: the complete reference. The MIT Press, Cambridge (1996)

    Google Scholar 

30. Walsh, T.: SAT versus CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 441–456. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

31. Zang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its applications to Quasigroup problems. Journal of Symbolic Computation 21, 543–560 (1996)

    Article  MathSciNet  MATH  Google Scholar 

32. 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. 2919, Springer, Heidelberg (2004)

    Google Scholar 

Download references