Research map / Learning theory and algorithms / Combinatorial and search optimization
CEGAR-Based Approach for Solving Combinatorial Optimization Modulo Quantified Linear Arithmetics Problems
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.
Proposes a CEGAR algorithm for combinatorial optimization modulo one level of universally quantified linear constraints (OPT+qLP), implemented as MERRINASP on clingo, and shows large speedups over Clingo[lpx] on biological rule-inference benchmarks.
Problem
Solving optimization problems that mix Boolean logic with universally quantified linear constraints (OPT+qLP), which arise in inferring metabolic regulatory rules; existing approaches rely on quantifier elimination followed by quantifier-free hybrid solvers.
Approach
Refine a Boolean abstraction of the OPT+qLP problem with counter-examples generalized via unsatisfiable cores (for existential constraints) and optimal cores exploiting monotonicity of LP optima (for universal constraints), plus partitioning of linear constraints into independent subsets.
Key results
- On large-scale instances MERRINASP outperforms Clingo[lpx] by a factor of 10 overall and by about 30x for finding the first model on satisfiable instances.
- Linear constraint partitioning speeds up MERRINASP by a factor of 1000 on satisfiable and 20 on unsatisfiable instances; no large-scale instance finished within 48 hours without partitioning.
- Counter-example generation for universal constraints (Q) is about 3x faster than quantifier elimination on small-scale and 20x on large-scale benchmarks; combined P and Q cut time by about 2000x.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Partition linear constraints (ablation) | MERRINASP · Small-SAT | Deciding SAT time (s): 5 528 ± 1 498 -> 9 ± 1 | Helped |
| Partition linear constraints (ablation) | MERRINASP · Small-UNSAT | Deciding SAT time (s): 247 ± 38 -> 10 ± 2 | Helped |
| Use quantified linear constraints instead of quantifier elimination (ablation) | MERRINASP · Small-SAT | Deciding SAT time (s): 28 ± 6 -> 9 ± 1 | Helped |
| Use quantified linear constraints instead of quantifier elimination (ablation) | MERRINASP · Small-UNSAT | Deciding SAT time (s): 30 ± 10 -> 10 ± 2 | Helped |
| Use quantified linear constraints instead of quantifier elimination (ablation) | MERRINASP · Large-SAT | Deciding SAT time (s): 3 163 ± 1 538 -> 183 ± 75 | Helped |
| Use quantified linear constraints instead of quantifier elimination (ablation) | MERRINASP · Large-UNSAT | Deciding SAT time (s): 739 ± 454 -> 135 ± 19 | Helped |
| Use MERRINASP instead of Clingo[lpx] | Large-scale OPT+qLP instances · Large-scale instances | runtime: factor of 10 | Helped |
| Use MERRINASP instead of Clingo[lpx] to find the first model | Large-scale satisfiable OPT+qLP instances · Large-SAT | time to first model: factor of 30 | Helped |
| Use partitioning and quantified linear constraints together (ablation) | MERRINASP · OPT+qLP benchmarks | computation time: 2 000 | Helped |
Surprising findings
- On enumeration of 100 models and on unsatisfiable instances, MERRINASP performs similarly to Clingo[lpx] rather than clearly better, because CEGAR requires many checks during enumeration.
Limitations
- Enumeration and unsatisfiable instances remain roughly on par with Clingo[lpx] due to many counter-example checks.
- MERRINASP is a prototype using Python PuLP with COIN LP solver and does not use incremental simplex.
- Linear constraint partitioning must currently be specified explicitly in the input problem.
Experimental setup
Datasets: metabolic regulatory rules inference benchmarks (small-scale from Thuillier et al. 2022; large-scale generated from a re
Benchmarks: OPT+qLP metabolic regulatory rules inference benchmark (120 instances: 60 small-scale, 60 large-scale)
Metrics: runtime (s) solved instances number of LP solver calls number of refinements
Baselines: Clingo[lpx] MERRINASP without partitioning (¬P, Q) MERRINASP with quantifier elimination (P, ¬Q) MERRINASP without partitioning or quantified constraints (¬P, ¬Q)
Builds on: CEGAR Clingo[lpx] quantifier elimination via LP strong duality clingo
Closest papers by meaning
- 2-ASP(Q) Solving Based on CEGAR (AAAI 2026 · similarity 0.86)
- OptiBench Meets ReSocratic: Measure and Improve LLMs for Optimization Modeling (ICLR 2025 · similarity 0.84)
- Scalable Enumeration of Trap Spaces in Boolean Networks via Answer Set Programming (AAAI 2024 · similarity 0.84)
- EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations (ICML 2025 · similarity 0.83)
- SolverLLM: Leveraging Test-Time Scaling for Optimization Problem via LLM-Guided Search (NeurIPS 2025 · similarity 0.83)
- $\texttt{STRCMP}$: Integrating Graph Structural Priors with Language Models for Combinatorial Optimization (NeurIPS 2025 · similarity 0.83)
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.