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

This paper proposes using Empirical Cumulative Distribution Functions to evaluate MaxSAT solvers' anytime performance, demonstrating that this approach reveals dynamic performance distinctions and enables automatic configurators like SMAC to discover superior parameter settings compared to traditional final-solution metrics.

The Gist

Imagine you are organizing a massive cooking competition to find the best recipe for a complex dish (let's call it the "MaxSAT Problem"). You have four famous chefs (the solvers: NuWLS, BandMax, MaxFPS, and SATLike) and a strict time limit of 5 minutes to cook.

The Old Way: The "Final Plate" Judgment

Traditionally, judges would only look at the final plate presented at the exact moment the 5-minute timer beeped.

• The Rule: "Whoever has the tastiest dish at 5:00 wins."
• The Problem: This ignores the journey. Did Chef A start with a burnt mess but slowly improve? Did Chef B have a great dish at 2 minutes but then accidentally dropped it? Did Chef C take a long time to prep but cook incredibly fast once started?
• The Result: By only looking at the final second, the judges might miss who is actually the most efficient or promising cook. They might declare two chefs "equal" because their final dishes look the same, even though one got there much faster.

The New Idea: The "Cooking Video" (Anytime Performance)

This paper suggests a better way to judge: Watch the whole cooking video.

Instead of just checking the dish at 5:00, the authors propose using a tool called ECDF (Empirical Cumulative Distribution Function). Think of this as a speedometer for quality.

• How it works: Instead of asking, "How good is the dish at 5 minutes?", we ask, "At what time did the chef reach 50% of their potential? 80%? 90%?"
• The Analogy: Imagine a graph where the X-axis is Time and the Y-axis is Quality.
  • Chef NuWLS might be a slow starter but climbs a steep hill, reaching high quality very quickly.
  • Chef BandMax might start fast but get stuck on a plateau.
  • Chef SATLike might be consistent but slow.
• The Benefit: This method reveals the "personality" of each solver. It shows that while NuWLS might be the best overall, BandMax might actually be the best if you only have 10 seconds. It turns a single score into a rich story of progress.

The "Magic Tuning Knob" (Hyperparameter Optimization)

Now, imagine these chefs have secret recipe books with adjustable knobs (parameters). To make them better, you need to tweak these knobs.

• The Old Tuning Method: You tweak the knobs, run the chef for 5 minutes, and see if the final dish is better. If two settings produce the same final dish, you can't tell which one was "smarter" or more efficient.
• The New Tuning Method (AUC): The authors used a tool called SMAC (a smart robot tuner). Instead of just looking at the final dish, the robot watched the entire cooking process (the ECDF curve).
  • It calculated the Area Under the Curve (AUC). Think of this as the total "deliciousness" accumulated over the whole 5 minutes.
  • The Discovery: When the robot tuned the chefs based on the whole video (AUC) rather than just the final plate, it found better settings!
  • Why? Because the "whole video" method gives the robot more clues. If two settings produce the same final dish, the one that got there faster (higher AUC) is clearly superior. The old method couldn't see the difference.

The Takeaway

1. Don't just look at the finish line. In complex problem-solving, how you get there matters just as much as where you end up.
2. NuWLS is the current champion, but the other chefs have their own strengths depending on how much time you give them.
3. Tuning with "Time" in mind works better. If you want to build the best AI solver, don't just ask, "Is the answer good?" Ask, "How fast and smoothly did it get to the answer?"

In a nutshell: This paper teaches us that to truly understand and improve these problem-solving algorithms, we need to stop treating them like a sprinter who only matters at the finish line, and start treating them like a marathon runner where the pace, the strategy, and the consistency throughout the race are what truly define the winner.

Technical Summary

1. Problem Definition

The paper addresses the Maximum Satisfiability (MaxSAT) problem, specifically the Weighted Partial MaxSAT (WPMS) variant, which involves finding an assignment that satisfies all "hard" clauses while maximizing the total weight of satisfied "soft" clauses.

While numerous Stochastic Local Search (SLS) solvers exist (e.g., SATLike, NuWLS), their performance is traditionally evaluated using fixed-budget metrics. These metrics assess the quality of the best-found solution at a single, specific cutoff time (e.g., 300 seconds). The authors argue that this approach has significant limitations:

• Bias: It ignores the convergence behavior of solvers during the optimization process.
• Loss of Information: Solvers that reach a high-quality solution quickly but stagnate may be rated identically to those that reach it slowly.
• Inadequate for Configuration: Fixed-budget metrics provide sparse feedback to automatic hyperparameter optimizers (HPO), making it difficult to distinguish between configurations that perform similarly at the final cutoff but differ in their search dynamics.

2. Methodology

The authors propose a shift from fixed-budget assessment to Anytime Performance Analysis using Empirical Cumulative Distribution Functions (ECDF).

A. Anytime Performance Metric (ECDF)

Instead of looking at a single point in time, the authors define the performance of a solver $A$ on an instance $i$ at time $t$ as the fraction of solutions in a reference set $\Phi_i$ that are not better than the best solution found by $A$ up to time $t$.

• Formula: $ECDF(A, i, t) = \frac{|\{ \phi \in \Phi_i \mid \phi \geq \phi_{A,i} \}|}{|\Phi_i|}$
• Reference Set ($\Phi_i$): Composed of solution costs visited by all solvers during experiments.
• Aggregation: ECDFs are calculated at 100 logarithmically spaced time points within the budget (0–300s) and aggregated across multiple problem instances.
• Quantitative Measure: The Area Under the Curve (AUC) of the ECDF is used as a single scalar value to represent the solver's overall anytime performance. This metric is ratio-scaled, allowing for aggregation across instances with different solution quality scales.

B. Experimental Setup

• Solvers: Four state-of-the-art SLS solvers were evaluated: SATLike3.0, BandMax, MaxFPS, and NuWLS.
• Datasets: Benchmarks from the 2022 and 2023 MaxSAT Evaluations (Weighted and Unweighted tracks).
• Hardware: AMD EPYC 7763 CPU, 1TB RAM, 300s cutoff time per run, 10 independent runs per instance.

C. Hyperparameter Optimization (HPO)

The authors investigated whether using the anytime performance metric (AUC) as a cost function for HPO yields better configurations than traditional fixed-budget metrics (Best-found solution quality).

• Tool: SMAC (Sequential Model-based Algorithm Configuration).
• Cost Functions Compared:
  1. Best-f: Quality of the best solution found at the cutoff.
  2. Norm-f: Normalized score based on the best solution.
  3. ECDF (AUC): The aggregated area under the ECDF curve.
• Process: Solvers were tuned on 20% of instances and validated on the full set.

3. Key Contributions

1. First Anytime Assessment of MaxSAT SLS: The paper introduces the first comprehensive anytime performance analysis for MaxSAT SLS solvers, moving beyond single-point evaluation.
2. Revealing Hidden Behaviors: The ECDF analysis reveals that solver rankings are not static; they change depending on the time budget. For example, a solver might outperform others in the first 10 seconds but fall behind later, a nuance invisible to fixed-budget metrics.
3. Quantitative Differentiation: ECDFs provide a ratio scale that can distinguish between solvers that appear identical under fixed-budget metrics (e.g., when both find the same best solution but at different speeds).
4. Superior HPO Cost Function: The study demonstrates that using AUC (Anytime Performance) as the cost function for hyperparameter optimization leads to significantly better solver configurations compared to using traditional best-solution quality metrics.

4. Experimental Results

Performance Assessment Findings

• NuWLS Dominance: NuWLS generally outperformed other solvers across both weighted and unweighted tracks.
• Dynamic Rankings:
  • MaxFPS vs. BandMax: MaxFPS slightly outperformed BandMax within the first 10 seconds, but their relative performance swapped as time increased for weighted instances.
  • Instance-Specific Behavior: On "decision-tree" instances, NuWLS got trapped in local optima after ~10s, whereas on "ParametricRBACMaintenance" instances, BandMax only surpassed SATLike after 100s.
• Variance: ECDFs showed much higher variance across instances than fixed-budget scores, providing a more granular view of algorithmic behavior.

Hyperparameter Optimization Findings

• Better Configurations: Tuning solvers using AUC resulted in configurations that outperformed those tuned with Best-f or Norm-f.
  • Anytime Performance: AUC-tuned configurations achieved the best ECDF in 6 out of 8 scenarios.
  • Fixed-Budget Performance: AUC-tuned configurations achieved the best final scores in 5 out of 8 scenarios.
• Magnitude of Improvement: For NuWLS and SATLike, AUC tuning yielded average improvements of 4% and 15%, respectively, over the second-best method. In scenarios where AUC did not win, the results were only 0.6% worse on average.
• Reasoning: AUC provides a denser search space for the optimizer. It can distinguish between two configurations that find the same final solution but do so at different speeds, whereas Best-f treats them as identical. Additionally, AUC is more robust to "lucky" results at a specific cutoff time.

5. Significance

• Algorithm Design: The anytime analysis provides actionable insights for developers to improve solver convergence strategies, particularly for handling local optima and early-stage search efficiency.
• Benchmarking: It establishes ECDF as a superior, universal metric for comparing iterative optimization algorithms, capable of aggregating performance across diverse problem instances without being biased by solution scales.
• Automated Configuration: The work proves that the choice of cost function in HPO is critical. Using anytime performance metrics leads to more robust and competitive solver configurations, suggesting a paradigm shift in how MaxSAT solvers (and potentially other iterative algorithms) should be tuned and evaluated.
• Generalizability: While focused on MaxSAT SLS, the methodology is transparent to hybrid solvers (combining complete and incomplete methods) and applicable to other black-box optimization domains.