Better Understandings and Configurations in MaxSAT Local Search Solvers via Anytime Performance Analysis

TL;DR

The paper tackles the limitation of evaluating MaxSAT solvers solely by best-found solutions within a fixed budget, proposing ECDF-based anytime performance as a more informative benchmarking tool. It analyzes four state-of-the-art SLS solvers (SATLike3.0, NuWLS, BandMax, MaxFPS) across MaxSAT tracks, showing that ECDFs reveal convergence behavior and instance-specific dynamics that fixed-budget metrics miss. The authors demonstrate that using aggregated ECDFs and the area under the ECDF (AUC) as a cost function in hyperparameter optimization with SMAC yields configurations that improve both anytime performance and fixed-budget outcomes in most scenarios. The results highlight the practical value of anytime-performance analysis for solver design and automatic configuration, with potential applicability to complete and hybrid solvers as well as portfolio approaches.

Abstract

Though numerous solvers have been proposed for the MaxSAT problem, and the benchmark environment such as MaxSAT Evaluations provides a platform for the comparison of the state-of-the-art solvers, existing assessments were usually evaluated based on the quality, e.g., fitness, of the best-found solutions obtained within a given running time budget. However, concerning solely the final obtained solutions regarding specific time budgets may restrict us from comprehending the behavior of the solvers along the convergence process. This paper demonstrates that Empirical Cumulative Distribution Functions can be used to compare MaxSAT stochastic local search solvers' anytime performance across multiple problem instances and various time budgets. The assessment reveals distinctions in solvers' performance and displays that the (dis)advantages of solvers adjust along different running times. This work also exhibits that the quantitative and high variance assessment of anytime performance can guide machines, i.e., automatic configurators, to search for better parameter settings. Our experimental results show that the hyperparameter optimization tool, i.e., SMAC, can achieve better parameter settings of solvers when using the anytime performance as the cost function, compared to using the metrics based on the fitness of the best-found solutions.

Figures (5)

• Figure 1: Heatmap illustrating the scores for individual instances. Each row represents an instance, while each column represents a different solver. The color depicts the score achieved by the solvers, with lighter shades indicating better performance. The benchmark tracks "MSE23-w", "MSE23-uw", "MSE22-w" and "MSE22-uw" consist of 160, 179, 197, and 179 instances (as shown by four boxes) respectively. The names of the instances have been omitted from the y-axis due to the limited space. Detailed results regarding groups of instances are available in Appendix B.
• Figure 2: An example of ECDF calculation. Left: The blue dots represent pairs $(t,\phi)$, where a better solution with fitness $\phi$ ($y$-axis) is obtained at time $t$ ($x$-axis). Right: the ECDF values based on the given set of solution fitness as presented in red stars on the left.
• Figure 3: Aggregated ECDFs of each solver for different sets of problem instances. $x$-axis indicates cpu time, and $y$-axis indicates the corresponding aggregated ECDF values.
• Figure 4: Heatmap illustrating aggregated ECDFs for individual instances. It follows the layout of Figure \ref{['fig:heatscore']}, but the color depicts the ECDF values achieved by the solvers. Detailed results regarding groups of instances are available in Appendix B.
• Figure 5: Aggregated ECDFs of the configurations obtained by tuning for Best-f, Norm-f, and ECDF for Left: MSE23-w and Right: MSE23-uw. Results plotted in one line are from five configurations obtained by independent runs of SMAC.