Dynamic Strategy to Diversify Search Using a History Map in Parallel Solving

  • Seongsoo Moon
  • Mary InabaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10079)


Diversification plays an important role in portfolio-based parallel SAT solvers. To maintain diversity, state-of-the-art solvers allocate different search policies and share learned clauses. However, the possibility of similarities between search space areas remains as learning progresses. In this paper we attempt to avoid frequently visited areas. We divide a search space into areas and convert each area into an index. We propose a heuristic to dynamically change the search space area using a history map of these indexes. The proposed heuristic was evaluated experimentally using the benchmarks from the application tracks of SAT-Race 2015.


  1. 1.
    Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21, 543–560 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Chrabakh, W., Wolski, R.: GrADSAT: a parallel SAT solver for the grid. Technical report, UCSB CS TR N (2003)Google Scholar
  3. 3.
    Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT 6(4), 245–262 (2009)zbMATHGoogle Scholar
  4. 4.
    Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel SAT solving. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 200–213. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31612-8_16 CrossRefGoogle Scholar
  5. 5.
    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). doi: 10.1007/978-3-642-15396-9_22 CrossRefGoogle Scholar
  6. 6.
    Blondel, V.D., Guillaume, J.-L., Lambiotte, R., Lefebvre, E.: Fast unfolding of communities in large networks. J. Stat. Mech.: Theory Exp. (2008). doi: Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.Tokyo UniversityTokyoJapan

Personalised recommendations