SAT-Based Techniques for Integer Linear Constraints

Conflict-Driven Clause-Learning (CDCL) SAT and SAT Modulo Theories (SMT) solvers are well known as workhorses for, e.g., formal verification applications. Here we discuss ways to go beyond by learning not only clauses, but also much more expressive constraints. We outline techniques for Integer Linear Programming (ILP), going first from SAT to SMT for ILP and then to SMT with on-the-fly bottleneck constraint encoding. Then we illustrate the power of learning full constraints, and the resulting methods for 0-1 ILP (Pseudo-Boolean solvers) and full ILP (Cutsat and IntSat), outlining difficulties and their solutions, giving examples and some intuition on why these techniques work so well.