Better Understandings and Configurations in MaxSAT Local Search Solvers via Anytime Performance Analysis
This work provides a more nuanced evaluation method for MaxSAT solvers, which is incremental but could benefit researchers and practitioners in optimization by improving solver configuration and understanding.
The paper tackled the problem of evaluating MaxSAT solvers by proposing the use of Empirical Cumulative Distribution Functions to analyze anytime performance, revealing performance distinctions and enabling better parameter configurations, with experiments showing that using anytime performance as a cost function in SMAC leads to improved solver settings compared to traditional fitness-based metrics.
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.