The predominance of multicore processors has increased the interest 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 solvers developed for Boolean optimization are scarce.
This dissertation proposes parallel search algorithms for Maximum Satisfiability (MaxSAT) and introduces PWBO, the first parallel solver for MaxSAT. PWBO can use two different strategies for parallel search. The first strategy performs a portfolio approach by searching on the lower and upper bound values of the optimal solution using different encodings of cardinality constraints for each thread. The second strategy splits the search space considering different upper bound values of the optimal solution for each thread.
As others parallel solvers, PWBO suffers from non-deterministic behavior, i.e. several runs of the same solver can lead to different solutions. This is a clear downside for applications that require solving the same problem instance more than once. Therefore, we also present the first deterministic parallel MaxSAT solver that ensures reproducibility of results. Finally, we also propose partitioning techniques to improve sequential MaxSAT algorithms.