Research map / Learning theory and algorithms / Combinatorial and search optimization
Automatic Core-Guided Reformulation via Constraint Explanation and Condition Learning
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.
Automates the core-guided objective reformulation pipeline of Leo et al. 2020 by explaining MaxSAT-style cores via MUS extraction, grouping them by explanation patterns, and learning conditions (LinearSVC scoring) to decide which objective terms to group, evaluated on RCPSP-WET.
Problem
SAT/CP solvers underperform on optimisation models whose objective is a sum of single-variable terms, and manually-derived core-guided reformulations are laborious because the causes of cores must be identified and lifted to model level by hand.
Approach
Automatically trace each core to its causing instance constraints via MUS enumeration and constraint paths, generalise explanations into patterns, and learn with a linear regressor which instantiations produce tight (core-generating) constraints so that only useful objective terms are grouped.
Key results
- Reformulation 300:1 (trained on easy instances, highest-scoring pattern) has solve/flatten geometric-mean ratios of 0.8/1.3 relative to the hand-written model.
- On instance 30_27_5 the automatic reformulation 111:A solves in 0.71s vs 0.52s original and 0.15s for hand-written H; naive reformulations were not faster than the original.
- Training on all patterns (e.g. 210:A) led to much higher training time (258s vs 60s) and worse flatten ratio (11.6) than using only the top pattern.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Automatically group objective terms using core patterns learned from 300 easy instances | RCPSP-WET · RCPSP-WET instances in Table 2 | solve time (s): 0.52 -> 0.15; 6.18 -> 0.70; 1.49 -> 0.30; 158.72 -> 0.79; TO -> 3.86 | Mixed |
| Use all learned patterns rather than only the highest-scoring pattern (ablation) | Automatic RCPSP-WET reformulation · RCPSP-WET | solve-time ratio (S): 0.8 -> 0.8; 1.0 -> 0.9; 1.0 -> 1.0; 0.9 -> 0.9 | No clear effect |
| Train on different instance mixes rather than 300 easy instances (ablation) | Automatic RCPSP-WET reformulation using the highest-scoring pattern · RCPSP-WET | solve-time ratio (S): 0.8 -> 1.0; 0.8 -> 0.9 | Mixed |
Surprising findings
- Using only the highest-scoring pattern produced faster training and faster flattening than using all patterns, though solve times were similar to the hand-written model.
- Naive reformulations that group terms in order of occurrence were not faster than the original model.
Limitations
- Only one MUS per core is extracted, so some explanations may be missed.
- Bounds for new variables in CP solvers are not yet automated (Step 3.2 not tackled), limiting performance on CP solvers.
- Evaluated on a single model (rcpsp-wet) with 12 instances.
Experimental setup
Datasets: rcpsp-wet MiniZinc benchmark instances (12 instances)
Benchmarks: rcpsp-wet MiniZinc benchmark instances
Metrics: geometric mean ratio of solve time to hand-reformulated mode flattening time ratio training time number of cores/explanations/patterns
Baselines: hand-written direct model (H) naive reformulation (N) weighted naive reformulation (NW) original rcpsp-wet model (O)
Builds on: Leo et al. 2020 core-guided reformulation OLL FindMUS Lazy Clause Generation most specific generalisation (Zeighami et al. 2018)
Closest papers by meaning
- Improving the Lower Bound in Branch-and-Bound Algorithms for MaxSAT (AAAI 2025 · similarity 0.86)
- HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation (NeurIPS 2024 · similarity 0.84)
- Better Understandings and Configurations in MaxSAT Stochastic Local Search Solvers via Anytime Performance Analysis (AAAI 2025 · similarity 0.84)
- PEARL: Solver-in-the-Loop Interactive Optimization Modeling from Natural Language (NeurIPS 2026 · similarity 0.83)
- SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.82)
- Theoretical and Empirical Analysis of Cost-Function Merging for Implicit Hitting Set WCSP Solving (AAAI 2024 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.