1. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. IJCAI9, 399–404 (2009)

   Google Scholar 

2. Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197–205. Springer, Heidelberg (2014)

   Google Scholar 

3. Belov, A., Diepold, D., Heule, M.J., Järvisalo, M.: Sat competition (2014)

   Google Scholar 

4. Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Balint, A., Belov, A., Heule, M.J.H., Järvisalo, M. (ed.), Proceedings of SAT Competition 2013, vol. B-2013-1 of Department of Computer Science Series of Publications B, pp. 51–52. University of Helsinki, 2013 (2013)

   Google Scholar 

5. Biere, A., Heule, M., van Maaren, H., Walsh, T.: Conflict-driven clause learning sat solvers. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pp. 131–153 (2009)

   Google Scholar 

6. Blochinger, W., Westje, W., Kuchlin, W., Wedeniwski, S.: Zetasat-boolean satisfiability solving on desktop grids. In: IEEE International Symposium on Cluster Computing and the Grid, 2005. CCGrid 2005, vol. 2, pp. 1079–1086. IEEE (2005)

   Google Scholar 

7. Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Communications of the ACM13(7), 422–426 (1970)

   Article MATH  Google Scholar 

8. Chrabakh, W., Wolski, R.: Gradsat: A parallel sat solver for the grid. In: Proceedings of IEEE SC03 (2003)

   Google Scholar 

9. Chrabakh, W., Wolski, R.: Gridsat: A chaff-based distributed sat solver for the grid. In: Proceedings of the 2003 ACM/IEEE conference on Supercomputing, p. 37. ACM (2003)

   Google Scholar 

10. Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

11. Gil, L., Flores, P., Silveira, L.M.: Pmsat: a parallel version of minisat. Journal on Satisfiability, Boolean Modeling and Computation6, 71–98 (2008)

    MathSciNet MATH  Google Scholar 

12. Gropp, W., Lusk, E., Doss, N., Skjellum, A.: A high-performance, portable implementation of the mpi message passing interface standard. Parallel computing22(6), 789–828 (1996)

    Article MATH  Google Scholar 

13. Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 252–265. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

14. Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel sat solver. Journal on Satisfiability, Boolean Modeling and Computation6, 245–262 (2008)

    MATH  Google Scholar 

15. Hölldobler, S., Manthey, N., Nguyen, V., Stecklina, J., Steinke, P.: A short overview on modern parallel sat-solvers. In: Proceedings of the International Conference on Advanced Computer Science and Information Systems, pp. 201–206 (2011)

    Google Scholar 

16. Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: Grid-Based SAT solving with iterative partitioning and clause learning. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 385–399. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

17. Hyvärinen, A.E., Junttila, T., Niemela, I.: Incorporating clause learning in grid-based randomized sat solving. Journal on Satisfiability, Boolean Modeling and Computation6, 223–244 (2014)

    MATH  Google Scholar 

18. Hyvärinen, A.E.J., Manthey, N.: Designing scalable parallel SAT solvers. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 214–227. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

19. Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355–370. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

20. Jurkowiak, B., Li, C.M., Utard, G.: A parallelization scheme based on work stealing for a class of sat solvers. Journal of Automated Reasoning34(1), 73–101 (2005)

    Article MathSciNet MATH  Google Scholar 

21. Kautz, H.A., Selman, B., et al.: Planning as satisfiability. ECAI92, 359–363 (1992)

    Google Scholar 

22. Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems21(12) (2002)

    Google Scholar 

23. Marques-Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers48(5), 506–521 (1999)

    Article MathSciNet  Google Scholar 

24. Martins, R., Manquinho, V., Lynce, I.: An overview of parallel sat solving. Constraints17(3), 304–347 (2012)

    Article MathSciNet MATH  Google Scholar 

25. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530–535. ACM (2001)

    Google Scholar 

26. Ohmura, K., Ueda, K.: c-sat: a parallel SAT solver for clusters. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 524–537. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

27. Parkes, A.J.: Clustering at the phase transition. In: Proc. of the 14th Nat. Conf. on AI, pp. 340–345. AAAI Press/The MIT Press (1997)

    Google Scholar 

28. Schulz, S., Blochinger, W.: Parallel sat solving on peer-to-peer desktop grids. Journal of Grid Computing8(3), 443–471 (2010)

    Article  Google Scholar 

29. Sorensson, N., Een, N.: Minisat v1.13 a sat solver with conflict-clause minimization. SAT 2005 (2005)

    Google Scholar 

30. Xu, L., Hoos, H., Leyton-Brown, K.: Hydra: Automatically configuring algorithms for portfolio-based selection. AAAI Conference on Artificial Intelligence (2010)

    Google Scholar 

Download references