AAAI’25 TUTORIAL ML FOR SOLVERS, PART II�MACHINE-LEARNING-BASED ALGORITHM SELECTION AND CONFIGURATION

Presenter: John Lu, Piyush Jha

Agenda

Introduction

​

Algorithm Selection

​

Algorithm Configuration

​

Active & Trending Areas

Motivation: Solvers show Complementary Strengths and Weaknesses

Different solver algorithms/parameters may favor different problem classes:

​

• Stochastic-search SAT solvers may have advantage in solving randomly generated satisfiable instances, but are usually outperformed by CDCL solvers upon large industrial instances (Kroening & Strichman, 2016).
• MapleSDCL (Oliveras et al., 2023) excels at hard problems such as Mutilated Chess Board (MCB), but not so well on some other classes.
• Int-blasting (Zohar et al., 2022) shows better performance than traditional bit-blasting-based solvers on SMT formulas involving large bit-vectors, but generally less effective on SMT-LIB QF_BV benchmarks.
• The optimal uniform restart rate highly depends on an instance’s problem class (Biere & Frölich, 2015).

​

Motivation: Solvers show Complementary Strengths and Weaknesses

results of SAT Competition 2024

Motivation: Leverage Complementary Strengths

Construct a near-VBS is hard:

​

• Few problem classes have known theoretically-proven best solving algorithms.
• Handcrafted selection strategies require tremendous expertise and effort.
• Real-world industrial instances are typically large and difficult to classify.
• The algorithm/solver space can be vast, especially considering the large number of tunable parameters.

Motivation: Leverage Complementary Strengths

To systematically find the optimal solver for a specific problem class/instance:

Data-Driven, Machine-Learning-Based

Algorithm Selection and Algorithm Configuration

Machine-Learning-Based Algorithm Selection

Algorithm

Selector

Machine-Learning-Based Algorithm Selection

Algorithm

Selector

Feature Representation

ML Models

ML training

Training

SATzilla (Xu et al., 2008): Pioneering Algorithm Selector for SAT

runtime prediction

SATzilla: Pioneering Algorithm Selector for SAT

EHM-based Algorithm Selection

……

SATzilla: Pioneering Algorithm Selector for SAT

Feature Representations for SAT instances (In total 48 features)

1. Problem size: #clauses, #variables, ratio
2. Variable-clause graph: variable & clause node degree stats
3. Variable graph: node degree stats
4. Balance: fraction of binary and ternary clauses…
5. Proximity to Horn formula: fraction of Horn clauses…
6. DPLL probing (with a short time): #unit propagations, search space estimate
7. Local search probing (with a short time)

Criteria: Correlate Well with Hardness, Cheap to Compute

SATzilla: Pioneering Algorithm Selector for SAT

SATzilla07 and SATzilla2009 won 5 medals in SAT comp 2007 and 2009, respectively.

Results from a recent work refactoring SATzilla (Shavit & Hoos, 2024):

​

On 2023 SAT comp benchmarks

SATzilla2024 closed 66% of the VBS-SBS gap

SATzilla2012 closed 53% of the gap

Btor2-Select (Lu et al., 2025): Algorithm Selection for Hardware Verification

A Hardware Model Checking Instance

(a) described in Btor2

(Niemetz et al., 2018)

(b) graph representation

Solvers

(tool.algorithm)

​

ABC.BMC

ABC.IMC

ABC.PDR

…

Pono.BMC

Pono.IMC

Pono.IC3

23

Btor2-Select: Algorithm Selection for Hardware Verification

Btor2 Verification Instance

A Simple Embedding

Bag of Keywords

(2, 1, …, 0, 1)

sort

state

zero

69 keywords

xor

Btor2-Select: Algorithm Selection for Hardware Verification

Relabel

sort → A

state → B

zero → C

……

Is there a computationally cheap representation can distinguish such two graphs?

A B C

A B C

Btor2-Select: Algorithm Selection for Hardware Verification

Weisfeiler-Lehman Graph Kernels (Shervashidze et al., 2011)

Iteration 0 (original)

Iteration 1

Multiset-label determination and sorting

Iteration 1

Label compression

A,B → D

A,C → E

B,AAC → F

B,AC → G

C,AB → H

C,B → I

Iteration 1

Relabeling

Btor2-Select: Algorithm Selection for Hardware Verification

Weisfeiler-Lehman Graph Kernels (Shervashidze et al., 2011)

Iteration 0

Iteration 1

WL(1) Feature Representations:

A B C D E F G H I

A B C D E F G H I

Iteratively, WL(2), WL(3), etc., can capture richer topological structural information.

Btor2-Select: Algorithm Selection for Hardware Verification

Evaluation

Btor2-Select outperforms:

• ABC.sc-PDR, the Single Best Solver
• super_prove, a handcrafted-crafted parallel solver based on different ABC configurations
• Btor2-PARA, a portfolio solver running three solvers in parallel

Algorithm Configuration

Automated search for the optimal parameter configuration of a parameterized algorithm.

​

Challenge: A solver may have numerous tunable parameters of different types, including categorical, integer, and continuous variables.

Example: $ Z3 -p

global parameters

[module] sat

……

……

[module] optimization

……

Algorithm Configuration

Algorithm Configuration

Algorithm Configuration

ParamILS: Model-Free Algorithm Configuration (Hutter et al., 2009)

Model-Free Search

Within some budgets, try different configurations and return the best one

​

Iterated Local Search

1. Initialize a configuration
2. Experiment with modifying a single parameter value, accepting new configuration once an improvement is observed
3. Repeat Step 2 until no single-parameter change yields an improvement

​

Adaptively Adjust #Sample Instances to Evaluate and Runtime Capping

Extended Algorithm Configuration: SMT Strategy Synthesis

Tactic

A well-defined reasoning step, which either preprocesses, transforms, or solves the given formula

Examples: simplify, solve-eqs, smt, sat, etc, in the SMT solver Z3 (De Moura, L., & Bjørner, N., 2008)

​

Strategy

An algorithmic recipe for selecting, sequencing, and parameterizing tactics.

Examples:

• (then simplify solve-eqs smt)
• (if (> num-consts 467) (then simplify sat) sat)
• (then (using-params simplify :elim_and true) smt)

​

Extended Algorithm Configuration: SMT Strategy Challenge

Z3alpha: MCTS for SMT Strategy Synthesis (Lu et al, 2024)

MDP Modelling of

Strategy Synthesis

A simplified context-free grammar (CFG)

<S> → <T> <S>

<S> → smt

<T> → simplify

<T> → aig

<S>

<T> <S>

simply <S>

simplify smt

R =eval(simplify smt) = 0.6

e.g., 60% of instances in S

are solved by this strategy

Z3alpha: MCTS for SMT Strategy Synthesis

Search 1

R = 0.6

Search 2

R = 0.7✓

Search 3

R = 0.4

……

Infinite space, we want to search “smartly”

Z3alpha: MCTS for SMT Strategy Synthesis

One MCTS Simulation

tree policy:

exploit & explore

Z3alpha: MCTS for SMT Strategy Synthesis

Results of SMT-COMP’24: Num of Correctly Solved Benchmarks

Won Awards in QF_Datatypes, QF_LinearIntArith, QF_NonLinearIntArith, QF_NonLinearRealArith

SMAC: Model-Based Algorithm Configuration (Hutter et al, 2011, Lindauer et al., 2022)

A Notebook Demo

Active & Trending Areas

Automated Feature Representation

• Image + CNN [Loreggia et al., 2016]
• Graph Neural Network (GNN) [Zhang et al, 2024]
• Large Language Model [Wu et al, 2024]

Online and Adaptive Learning

• Online Learning: No prior knowledge, learn online when solving a series of instances [Degroote et al., 2016; Pimpalkhare et al., 2021]
• Adaptive Learning: Learning during solving a specific instance [Biedenkapp et al., 2020; Scott et al., 2022]

Theoretical Work

• PAC learnability, sample size requirement [Balcan et al, 2021]
• Performance guarantee with bounded runtime [Graham et al, 2023, Graham & Leyton-Brown, 2025]

Summary

• Algorithm Space: Solver, Parameter, Tactic…
• Scope: Per-Instance, Per-Set
• Learning Setting: Offline, Online
• Adjustment: Fixed, Adaptive

Hope you find this tutorial helpful!

1. Using algorithm selection & configuration for your own problem
2. Excited to work on this interdisciplinary topic

Reference

[Balcan et al., 2024] Balcan, M. F., Deblasio, D., Dick, T., Kingsford, C., Sandholm, T., & Vitercik, E. (2024). How Much Data Is Sufficient to Learn High-Performing Algorithms?. Journal of the ACM.

[Balcan et al., 2017] Balcan, M. F., Nagarajan, V., Vitercik, E., & White, C. (2017). Learning-theoretic foundations of algorithm configuration for combinatorial partitioning problems. COLT 2017.

[Balcan et al., 2021] Balcan, M. F., Sandholm, T., & Vitercik, E. (2021). Generalization in portfolio-based algorithm selection. AAAI 2021.

[Biedenkapp et al., 2020] Biedenkapp, A., Bozkurt, H. F., Eimer, T., Hutter, F., & Lindauer, M. (2020). Dynamic algorithm configuration: Foundation of a new meta-algorithmic framework. ECAI 2020.

[Biere & Frölich, 2015] Biere, A., & Fröhlich, A. (2015). Evaluating CDCL restart schemes. Proceedings of Pragmatics of SAT, 1-17.

[Degroote, 2017] Online Algorithm Selection. IJCAI 2017.

[De Moura & Bjørner, 2008] De Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. TACAS 2008.

[De Moura & Passmore, 2013] De Moura, L., & Passmore, G. O. (2013). The strategy challenge in SMT solving. Automated Reasoning and Mathematics: Essays in Memory of William W. McCune.

[Graham et al., 2023] Graham, D., Leyton-Brown, K., & Roughgarden, T. (2023). Utilitarian algorithm configuration. NeurIPS 2023.

[Graham & Leyton-Brown, 2025] Graham, D., & Leyton-Brown, K. (2025). Utilitarian Algorithm Configuration for Infinite Parameter Spaces. ICLR 2025.

[Gupta & Roughgarden, 2017] Gupta, R., & Roughgarden, T. (2016). A PAC approach to application-specific algorithm selection. SIAM J. Comput.

[Hutter et al., 2009] Hutter, F., Hoos, H. H., Leyton-Brown, K., & Stützle, T. (2009). ParamILS: an automatic algorithm configuration framework. Journal of artificial intelligence research.

[Hutter et al., 2011] Hutter, F., Hoos, H. H., & Leyton-Brown, K. (2011). Sequential model-based optimization for general algorithm configuration. LION 5.

[Kroening & Strichman, 2016] Kroening, D., & Strichman, O. Decision Procedures - An Algorithmic Point of View (2nd ed.). Texts in Theoretical Computer Science. An EATCS Series. Springer.

[Leeson & Dwyer, 2024] Leeson, W., & Dwyer, M. B. (2024). Algorithm Selection for Software Verification using Graph Neural Networks. ACM Transactions on Software Engineering and Methodology.

[Lindauer et al., 2022] Lindauer, M., Eggensperger, K., Feurer, M., Biedenkapp, A., Deng, D., Benjamins, C., Ruhkopf, T., Sass, R., & Hutter, F. (2022). SMAC3: A versatile Bayesian optimization package for hyperparameter optimization. Journal of Machine Learning Research.

[Loreggia et al., 2016] Loreggia, A., Malitsky, Y., Samulowitz, H., & Saraswat, V. (2016). Deep learning for algorithm portfolios. AAAI 2016.

[Lu et al., 2024] Lu, Z., Siemer S., Jha P., Day J., Manea F., & Ganesh, V. (2024). Layered and staged Monte Carlo Tree Search for SMT strategy synthesis. IJCAI 2024.

[Lu et al., 2025] Lu, Z., Chien, P., Lee, N., & Ganesh, V. (2025) Algorithm selection for word-level hardware model checking. AAAI 2025.

[Niemetz, A., 2018] Niemetz, A., Preiner, M., Wolf, C., & Biere, A. (2018). Btor2, BtorMC and Boolector 3.0. CAV 2018.

[Nudelman et al., 2004] Nudelman, E., Leyton-Brown, K., Hoos, H. H., Devkar, A., & Shoham, Y. (2004). Understanding random SAT: Beyond the clauses-to-variables ratio. CP 2004.

Reference

[Oliveras et al., 2023] Oliveras, A., Li, C., Wu, D., Chung, J., & Ganesh, V. (2023). Learning Shorter Redundant Clauses in SDCL Using MaxSAT. SAT 2023.

[Pimpalkhare et al., 2021] Pimpalkhare, N., Mora, F., Polgreen, E., & Seshia, S. A. (2021). MedleySolver: online SMT algorithm selection. SAT 2021.

[Scott et al., 2021] Scott, J., Niemetz, A., Preiner, M., Nejati, S., & Ganesh, V. (2021). MachSMT: A machine learning-based algorithm selector for SMT solvers. TACAS 2021.

[Scott et al., 2022] Scott, J., Pan, G., Khalil, E. B., & Ganesh, V. (2022). Goose: A Meta-Solver for Deep Neural Network Verification. SMT 2024.

[Shervashidze, N., 2011] Shervashidze, N., Schweitzer, P., Van Leeuwen, E. J., Mehlhorn, K., & Borgwardt, K. M. (2011). Weisfeiler-lehman graph kernels. Journal of Machine Learning Research.

[Wu et al., 2024] Wu, X., Zhong, Y., Wu, J., Jiang, B., & Tan, K. C. (2024). Large language model-enhanced algorithm selection: towards comprehensive algorithm representation. IJCAI 2024.

[Xu et al., 2008] Xu, L., Hutter, F., Hoos, H. H., & Leyton-Brown, K. (2008). SATzilla: portfolio-based algorithm selection for SAT. Journal of artificial intelligence research.

[Xu et al., 2012] Xu, L., Hutter, F., Hoos, H. H., & Leyton-Brown, K. (2012). Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors. SAT 2012.

[Zhang, Z. et al., 2024] Zhang, Z. et al. (2024). Grass: Combining graph neural networks with expert knowledge for SAT solver selection. ACM SIGKDD 2024.

[Zohar et al., 2022] Zohar, Y., Irfan, A., Mann, M., Niemetz, A., Nötzli, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2022). Bit-precise reasoning via int-blasting. CAV 2022.

​

Appendix: Algorithm Configuration Through a Lens of Learning Theory

Appendix: Algorithm Configuration Through a Lens of Learning Theory

​

Research Question: Generalization Error Bound and Required Sample Size (Balcan et al., 2017; Balcan et al., 2024)

​

Research Question: Generalization Error Bound for Per-Instance Algorithm Selection (Balcan et al., 2021)

……