Research map / Learning theory and algorithms / Combinatorial and search optimization
SAT-Based Tree Decomposition with Iterative Cascading Policy Selection
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.
Configures the TW-SLIM SAT-based local improvement framework for treewidth minimization using offline clustering-based configuration plus dynamic real-time selection, and proposes an iterative cascading policy (ICP) over 30 configurations that outperforms hand-tuned defaults and SMAC/AutoFolio baselines.
Problem
Choosing critical parameters (local budget, local time, SAT time, switch flag) for SAT-based local improvement frameworks such as TW-SLIM, whose performance depends heavily on configuration and changes as the instance evolves during the run.
Approach
Combine constrained-clustering-based offline configuration (30 configurations, one per cluster) with dynamic, round-based cascading orderings chosen by instance features, retaining the best tree decomposition after each round, so the configuration sequence adapts to the changing instance.
Key results
- Iterative cascading policy ICP-sta (TΣ) reaches TΣ = 728 at the 7800-second timeout versus 398 for hand-tuned TW-SLIM on the test set, and is ahead of SB-all (457) and CA (456).
- Within the 100-second timeout, ICP-sta (TΣ) reaches 361/168 (TΣ/T#) versus 234/132 for CC-sta and 223/128 for CC-dyn.
- Clustering-based CC-sta raises TΣ from 398 to 500 on test instances at 7800 seconds, outperforming the AutoFolio-based selector.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use iterative cascading with a static cascade sorted by TΣ instead of the hand-tuned configuration | TW-SLIM · MINTW test set, 7800s timeout | TΣ: 398 -> 728 | Helped |
| Use iterative cascading with a static cascade sorted by TΣ instead of offline single-best tuning | TW-SLIM · MINTW test set, 7800s timeout | TΣ: 457 -> 728 | Helped |
| Adapt cascade ordering to updated instance features rather than keep it static (ablation) | TW-SLIM with ICP · MINTW test set, 7800s timeout | TΣ: 728 -> 712 | Hurt |
| Adapt cascade ordering to updated instance features rather than keep it static (ablation) | TW-SLIM with ICP · MINTW test set, 100s timeout | TΣ: 361 -> 296 | Hurt |
| Sort static cascade priority by T# instead of TΣ (ablation) | TW-SLIM with ICP · MINTW test set, 7800s timeout | TΣ: 728 -> 691 | Hurt |
| Sort dynamic cascade priority by T# instead of TΣ (ablation) | TW-SLIM with ICP · MINTW test set, 100s timeout | TΣ: 296 -> 338 | Helped |
| Sort dynamic cascade priority by T# instead of TΣ (ablation) | TW-SLIM with ICP · MINTW test set, 7800s timeout | TΣ: 712 -> 710 | No clear effect |
| Filter out configurations with unique-best count ub = 0 (ablation) | TW-SLIM with static ICP · MINTW test set, 100s timeout | TΣ: 361 -> 364 | Helped |
| Filter out configurations with unique-best count ub = 0 (ablation) | TW-SLIM with static ICP · MINTW test set, 7800s timeout | TΣ: 728 -> 724 | No clear effect |
| Use dynamic clustering-based configuration selection instead of static clustering-based selection | TW-SLIM · MINTW test set, 7800s timeout | TΣ: 500 -> 619 | Helped |
| Use dynamic clustering-based configuration selection instead of static clustering-based selection | TW-SLIM · MINTW test set, 100s timeout | TΣ: 234 -> 223 | Hurt |
| Use iterative cascading instead of dynamic clustering-based configuration selection | TW-SLIM · MINTW test set, 7800s timeout | TΣ: 619 -> 728 | Helped |
Surprising findings
- Dynamic configuration (CC-dyn) performs worse than the static CC-sta at timeouts below 500 seconds due to trial-and-error exploration.
- The AutoFolio-based algorithm selector (CA) performs worse than the clustering-based static configuration CC-sta, contrary to results in MaxSAT configuration.
Limitations
- Evaluated only on the treewidth problem (MINTW) with TW-SLIM, so generalization to other SLIM problems is untested.
- Dynamic configuration can deteriorate at short timeouts because of exploration overhead.
Experimental setup
Datasets: functions (sdcc.sourceforge.net) PACE16 PACE17 UAI Roadnet TWlib
Benchmarks: 3331 benchmark graphs (667 test graphs)
Metrics: TΣ (total sum of treewidth improvements) T# (number of improved instances)
Baselines: hand-tuned TW-SLIM SB-all (SMAC) Cluster-AutoFolio (CA) SB-one CC-dyn CC-sta
Builds on: TW-SLIM cascading portfolio scheduling SMAC AutoFolio
Closest papers by meaning
- MixSATGEN: Learning Graph Mixing for SAT Instance Generation (ICLR 2024 · similarity 0.88)
- On Continuous Local BDD-Based Search for Hybrid SAT Solving (AAAI 2021 · similarity 0.88)
- A Scalable Two Stage Approach to Computing Optimal Decision Sets (AAAI 2021 · similarity 0.87)
- DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem (AAAI 2025 · similarity 0.87)
- Parameterization of (Partial) Maximum Satisfiability above Matching in a Variable-Clause Graph (AAAI 2024 · similarity 0.85)
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.85)
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.