# Encoding Linear Constraints into SAT

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 May 2020.

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

- [Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints](https://mlsanity.com/paper/2307.09342/) (2023)
- [Planning with Learned Binarized Neural Networks Benchmarks for MaxSAT Evaluation 2021](https://mlsanity.com/paper/2108.00633/) (2021)

## Abstract (arXiv)

Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of conjunctive normal form perform poorly in problems with these constraints in comparison with SAT modulo theories (SMT), lazy clause generation (LCG) or mixed integer programming (MIP) solvers. In this paper we explore and categorize SAT encodings for linear integer constraints. We define new SAT encodings based on multi-valued decision diagrams, and sorting networks. We compare different SAT encodings of linear constraints and demonstrate where one may be preferable to another. We also compare SAT encodings against other solving methods and show they can be better than linear integer (MIP) solvers and sometimes better than LCG or SMT solvers on appropriate problems. Combining the new encoding with lazy decomposition, which during runtime only encodes constraints that are important to the solving process that occurs, gives the best option for many highly combinatorial problems involving linear constraints.