Monte-Carlo Tree Search for the Maximum Satisfiability Problem

Incomplete algorithms for the Maximum Satisfiability (MaxSAT) problem use a hill climbing approach in tandem with various mechanisms that prevent search stagnation. These solvers' conflicting goals of maintaining search mobility while discovering high quality solutions constitute an exploration-exploitation dilemma, a problem which has been tackled with great success in recent years using Monte-Carlo Tree Search (MCTS) methods. We apply MCTS to the domain of MaxSAT using various stochastic local search (SLS) algorithms for leaf node value estimation, thus offering a novel hybrid alternative to established complete and incomplete solution techniques. Our algorithm outperforms baseline SLS algorithms like Walksat and Novelty on most problem instances from the 2015 MaxSAT Evaluation. It also outdoes CCLS, a state-of-the-art incomplete MaxSAT solver, on a number of challenging industrial instances from the 2015 MaxSAT Evaluation.