Affiliations: IST/INESC-ID, Technical University of Lisbon, Lisbon, Portugal. E-mails: {ruben, vmm, ines}@sat.inesc-id.pt
Note: [] Corresponding author: Ruben Martins, IST/INESC-ID, Technical University of Lisbon, Rua Alves Redol 9, 1000-029 Lisbon, Portugal. E-mail: ruben@sat.inesc-id.pt.
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 approaches developed for Boolean optimization are scarce. This paper proposes parallel search algorithms for Maximum Satisfiability (MaxSAT) and introduces PWBO, a new parallel solver for partial MaxSAT. Using two threads, an unsatisfiability-based algorithm is used to search on the lower bound of the optimal solution, while at the same time a linear search is performed on the upper bound of the optimal solution. Moreover, learned clauses are shared between threads during the search. For a larger number of threads two different strategies are proposed. 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. Experimental results show that the techniques proposed in the paper enable PWBO to improve when increasing the number of threads.
Keywords: Parallel search, maximum satisfiability, cardinality constraints
