DistMS: A Non-Portfolio Distributed Solver for Maximum Satisfiability
This addresses scalability problems for users of parallel MaxSAT solvers, but it is incremental as it builds on existing distributed solving approaches.
The paper tackles the issues of memory contention and scalability in multicore parallel MaxSAT solvers by introducing DistMS, a non-portfolio distributed solver. Preliminary results indicate that it outperforms its sequential version and solves more instances as processes increase.
The most successful parallel SAT and MaxSAT solvers follow a portfolio approach, where each thread applies a different algorithm (or the same algorithm configured differently) to solve a given problem instance. The main goal of building a portfolio is to diversify the search process being carried out by each thread. As soon as one thread finishes, the instance can be deemed solved. In this paper we present a new open source distributed solver for MaxSAT solving that addresses two issues commonly found in multicore parallel solvers, namely memory contention and scalability. Preliminary results show that our non-portfolio distributed MaxSAT solver outperforms its sequential version and is able to solve more instances as the number of processes increases.