# Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints

arXiv: https://arxiv.org/abs/2307.09342 · HTML: https://mlsanity.com/paper/2307.09342/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 49 references that are in the map.
- First posted on arXiv 18 Jul 2023.

## Builds on (most cited first, 9 of 9)

- [XGBoost: A Scalable Tree Boosting System](https://mlsanity.com/paper/1603.02754/) (2016)
- [Automated Algorithm Selection: Survey and Perspectives](https://mlsanity.com/paper/1811.11597/) (2018)
- [Hyperparameters and Tuning Strategies for Random Forest](https://mlsanity.com/paper/1804.03515/) (2018)
- [A New Look at BDDs for Pseudo-Boolean Constraints](https://mlsanity.com/paper/1401.5860/) (2014)
- [Generalized Totalizer Encoding for Pseudo-Boolean Constraints](https://mlsanity.com/paper/1507.05920/) (2015)
- [An Enhanced Features Extractor for a Portfolio of Constraint Solvers](https://mlsanity.com/paper/1308.0227/) (2013)
- [Proteus: A Hierarchical Portfolio of Solvers and Transformations](https://mlsanity.com/paper/1306.5606/) (2013)
- [SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints](https://mlsanity.com/paper/2110.08068/) (2021)
- [Encoding Linear Constraints into SAT](https://mlsanity.com/paper/2005.02073/) (2020)

## Built on by (most cited first, 2 of 2)

- [An Exhaustive DPLL Approach to Model Counting over Integer Linear Constraints with Simplification Techniques](https://mlsanity.com/paper/2509.13880/) (2025)
- [Partition Scores Are Not System Scores: Deployment-Fidelity Gaps in Decomposed Algorithm Selection](https://mlsanity.com/paper/2609.13785/) (2026)

## Abstract (arXiv)

Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudo-Boolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems; however we obtain better performance with a new set of features specifically designed for the pseudo-Boolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method.