Parallel Search for Maximum Satisfiability

Author

Ruben Martins

School

Instituto Superior Técnico, Universidade de Lisboa, Portugal

Supervisors

Inês Lynce
Vasco Manquinho

Abstract

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.

Graduated

Notes

Awards of the solvers developed during my PhD (WBO and PWBO): 1 bronze medal at PB Evaluation 2011; 2 silver medals and 1 bronze medal at MaxSAT Evaluation 2011; 2 gold medals, 1 silver medal and 1 bronze medal at MaxSAT Evaluation 2012.