Learning SMT(LRA) Constraints using SMT Solvers

Learning SMT(LRA) Constraints using SMT Solvers

Samuel Kolb, Stefano Teso, Andrea Passerini, Luc De Raedt

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Main track. Pages 2333-2340. https://doi.org/10.24963/ijcai.2018/323

We introduce the problem of learning SMT(LRA) constraints from data. SMT(LRA) extends propositional logic with (in)equalities between numerical variables. Many relevant formal verification problems can be cast as SMT(LRA) instances and SMT(LRA) has supported recent developments in optimization and counting for hybrid Boolean and numerical domains. We introduce SMT(LRA) learning, the task of learning SMT(LRA) formulas from examples of feasible and infeasible instances, and we contribute INCAL, an exact non-greedy algorithm for this setting. Our approach encodes the learning task itself as an SMT(LRA) satisfiability problem that can be solved directly by SMT solvers. INCAL is an incremental algorithm that achieves exact learning by looking only at a small subset of the data, leading to significant speed-ups. We empirically evaluate our approach on both synthetic instances and benchmark problems taken from the SMT-LIB benchmarks repository.
Keywords:
Machine Learning: Relational Learning
Machine Learning: New Problems
Constraints and SAT: Constraints and Data Mining ; Machine Learning