Moving between high-quality optima using multi-satisfiability characteristics in hard-to-solve Max3Sat instances
J. Piatek, M. W. Przewozniczek, F. Chicano, R. Tinós
TL;DR
The paper tackles the challenge of solving hard Max3Sat instances by exploiting gray-box information and backbone structure. It introduces MOCSM, a clause-satisfiability manipulation-based optimizer that augments MMST and directed local search with a LongConnection mechanism to bridge distant high-quality regions in the search space. Backbone-based analysis motivates the design, linking instance features to solver effort and enabling a principled difficulty metric. Empirically, MOCSM outperforms state-of-the-art gray-box optimizers on hard instances while maintaining robustness on easier cases, and the proposed difficulty measure correlates with the required optimization budget. The work advances both practical solvers for Max3Sat and methodological insights for benchmarking and instance characterization.
Abstract
Gray-box optimization proposes effective and efficient optimizers of general use. To this end, it leverages information about variable dependencies and the subfunction-based problem representation. These approaches were already shown effective by enabling \textit{tunnelling} between local optima even if these moves require the modification of many dependent variables. Tunnelling is useful in solving the maximum satisfiability problem (MaxSat), which can be reformulated to Max3Sat. Since many real-world problems can be brought to solving the MaxSat/Max3Sat instances, it is important to solve them effectively and efficiently. Therefore, we focus on Max3Sat instances for which tunnelling fails to introduce improving moves between locally optimal high-quality solutions and the region of globally optimal solutions. We analyze the features of such instances on the ground of phase transitions. Based on these observations, we propose manipulating clause-satisfiability characteristics that allow connecting high-quality solutions distant in the solution space. We utilize multi-satisfiability characteristics in the optimizer built from typical gray-box mechanisms. The experimental study shows that the proposed optimizer can solve those Max3Sat instances that are out of the grasp of state-of-the-art gray-box optimizers. At the same time, it remains effective for instances that have already been successfully solved by gray-box.