DistMS: A Non-Portfolio Distributed Solver for Maximum Satisfiability

TL;DR

DistMS introduces a non-portfolio distributed MaxSAT solver that improves scalability and reduces memory contention, outperforming sequential versions and solving more instances with increased processes.

Contribution

This paper presents a novel non-portfolio distributed MaxSAT solver addressing memory contention and scalability issues in multicore parallel solvers.

Findings

Outperforms its sequential version.

Solves more instances as processes increase.

Reduces memory contention in parallel MaxSAT solving.

Abstract

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.