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.
展开▼
