Dynamic Strategy to Diversify Search Using a History Map in Parallel Solving
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.
- 2.Chrabakh, W., Wolski, R.: GrADSAT: a parallel SAT solver for the grid. Technical report, UCSB CS TR N (2003)Google Scholar
- 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:http://dx.doi.org/10.1088/1742-5468/2008/10/P10008 Google Scholar