Abstract
The Partial Max-SAT (PMSAT) problem is an optimization variant of the well-known Propositional Boolean Satisfiability (SAT) problem. It holds an important place in theory and practice, because a huge number of real-world problems, such as timetabling, planning, routing, bioinformatics, fault diagnosis, etc., could be encoded into it. Stochastic local search (SLS) methods can solve many real-world problems that often involve large-scale instances at reasonable computation costs while delivering good-quality solutions. In this work, we propose a novel SLS algorithm called adaptive variable depth SLS for PMSAT problem solving based on a dynamic local search framework. Our algorithm exploits two algorithmic components of an SLS method: parameter tuning and neighborhood search. Our first contribution is the design of an adaptive parameter tuner that searches for the best parameter setting for each instance by considering its features. The second contribution is a variable depth neighborhood search (VDS) algorithm adopted for PMSAT problem, which our empirical evaluation proves is a more efficient w.r.t. single neighborhood search. We conducted our experiments on the PMSAT benchmarks from MaxSAT Evaluation 2014 to 2019, including more than 3600 instances which have been encoded from a broad range of domains such as verification, optimization, graph theory, automated-reasoning, pseudo Boolean, etc. Our experimental evaluation results show that AVD-SLS solver, which is implemented based on our algorithm, outperforms state-of-the-art PMSAT SLS solvers in most benchmark classes, including random, crafted, and industrial instances. Furthermore, AVD-SLS reports remarkably better results on weighted benchmark, and shows competitive results with several well-known hybrid PMSAT solvers.