Parallel Search for Boolean Optimization
Ruben Martins, Vasco M. Manquinho · 2011
Abstract. The predominance of multicore processors has increased the inter-est in developing parallel Boolean Satisfiability (SAT) solvers. As a result, more parallel SAT solvers are emerging. Even though parallel approaches are known to boost performance, parallel approaches developed for Boolean optimization are scarce. This paper proposes parallel search algorithms for Boolean optimiza-tion and introduces a new parallel solver for Boolean optimization problem in-stances. Using two threads, an unsatisfiability-based algorithm is used to search on the lower bound value of the objective function, while at the same time a linear search is performed on the upper bound value of the objective function. Searching in both directions and exchanging learned clauses between these two orthogonal approaches makes the search more efficient. This idea is further extended for a larger number of threads by dividing the search space considering different local upper values of the objective function. The parallel search on different local up-per values leads to constant updates on the lower and upper bound values, which result in reducing the search space. Moreover, different search strategies are per-formed on the upper bound value, increasing the diversification of the search. 1