Research map / Learning theory and algorithms / Combinatorial and search optimization

Theoretical and Empirical Analysis of Cost-Function Merging for Implicit Hitting Set WCSP Solving

AAAI 2024 · Learning theory and algorithms › Combinatorial and search optimization · approach: Unsupervised neural combinatorial optimization · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Analyzes the Implicit Hitting Set WCSP solver (HS-WCSP) theoretically via distinguished cores and proposes symbolic and numeric cost-function merging, showing exponential-to-constant iteration reductions on toy problems and speedups on Spot5 benchmarks.

Problem

HS-WCSP solvers can require an exponential number of iterations on WCSPs with symmetric or interchangeable cores, limiting their practical efficiency compared with MaxSAT.

Approach

Derives lower and upper bounds on HS-WCSP iterations via distinguished cores, identifies symbolic and numeric core interchangeability, and reformulates WCSPs by merging cost functions (symbolic counting or numeric summation) to make the core space compact, with tree-decomposition clustering used to pick merge groups on real instances.

Key results

• On GreaterThan, numeric merging reduces HS-WCSP iterations from exponential (Ω(4^(n-1)/√(πn))) to a single iteration, and symbolic merging to Ω((13.0019...)^√n / n).
• On the Spot5 benchmark, both symbolic and numeric merging solve more instances and faster than the original HS-WCSP, and both outperform Toulbar2 on all instances except two solved in under a second by all formulations.
• Merging can accelerate HS by several orders of magnitude on the typical benchmark problems, per the abstract.

Measured effects reported in the paper

Surprising findings

• The number of iterations is not always a good proxy for performance, since with the totalizer encoding the CPU cost of SAT calls can dominate.

Limitations

• Theoretical bounds are asymptotic and the symmetric case-study problems are artificial.
• Merging works only on small subsets of cost functions because the SAT encoding of sums (totalizer) becomes expensive as merged groups grow.
• The tree-decomposition-based clustering heuristic is a static pre-process and is not tuned beyond a min-fill heuristic.

Experimental setup

Datasets: GreaterThan problem (synthetic) AllDiff problem (synthetic) Spot5 WCSP benchmark

Benchmarks: GreaterThan AllDiff Spot5

Metrics: number of iterations number of SAT calls CPU time lower bound at timeout

Baselines: HS-WCSP original encoding Toulbar2

Builds on: HS-WCSP (Delisle and Bacchus 2013) implicit hitting set for MaxSAT abstract cores (Berg, Bacchus, and Poole 2020)

Closest papers by meaning

• Better Understandings and Configurations in MaxSAT Stochastic Local Search Solvers via Anytime Performance Analysis (AAAI 2025 · similarity 0.85)
• SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.82)
• Improving the Lower Bound in Branch-and-Bound Algorithms for MaxSAT (AAAI 2025 · similarity 0.82)
• Enhance Diversified Top-k MaxSAT Solving by Incorporating New Strategy for Generating Diversified Initial Assignments (Student Abstract) (AAAI 2024 · similarity 0.82)
• Fast, Scalable, Warm-Start Semidefinite Programming with Spectral Bundling and Sketching (ICML 2024 · similarity 0.82)
• Differentiable extensions with rounding guarantees for combinatorial optimization over permutations (NeurIPS 2025 · similarity 0.82)