Towards Tackling MaxSAT by Combining Nested Monte Carlo with Local Search

TL;DR

This paper enhances the UCTMAXSAT algorithm for MaxSAT by integrating Nested Monte Carlo Search and dynamic SLS budget adjustment, leading to improved and more robust performance across benchmark instances.

Contribution

Introduces two algorithmic variations over UCTMAXSAT, including Nested Monte Carlo Search and dynamic flip limit adjustment, with empirical validation on MaxSAT benchmarks.

Findings

Nested Monte Carlo improves performance on most instances.

Dynamic flip limit setting achieves robustness without tuning.

Empirical results show performance gains over previous methods.

Abstract

Recent work proposed the UCTMAXSAT algorithm to address Maximum Satisfiability Problems (MaxSAT) and shown improved performance over pure Stochastic Local Search algorithms (SLS). UCTMAXSAT is based on Monte Carlo Tree Search but it uses SLS instead of purely random playouts. In this work, we introduce two algorithmic variations over UCTMAXSAT. We carry an empirical analysis on MaxSAT benchmarks from recent competitions and establish that both ideas lead to performance improvements. First, a nesting of the tree search inspired by the Nested Monte Carlo Search algorithm is effective on most instance types in the benchmark. Second, we observe that using a static flip limit in SLS, the ideal budget depends heavily on the instance size and we propose to set it dynamically. We show that it is a robust way to achieve comparable performance on a variety of instances without requiring additional tuning.