Clustering-Guided SMT(LRA) Learning

Published in International Conference on integrated Formal Methods, 2020

In the SMT(LRA) learning problem, the goal is to learn SMT(LRA) constraints from real-world data. To improve the scalability of SMT(LRA) learning, we present a novel approach called SHREC which uses hierarchical clustering to guide the search, thus reducing runtime. A designer can choose between higher quality (SHREC1) and lower runtime (SHREC2) according to their needs. Our experiments show a significant scalability improvement and only a negligible loss of accuracy compared to the current state-of-the-art.

Download here