Skip to main content Skip to main navigation

Publication

Clustering-Guided SMT(LRA) Learning

Tim Meywerk; Marcel Walter; Daniel Große; Rolf Drechsler
In: 16th International Conference on integrated Formal Methods (iFM). International Conference on Integrated Formal Methods (IFM-2020), November 16-20, Lugano, Switzerland, 2020.

Abstract

In the SMT(LRA) learning problem, the goal is to learnSMT(LRA) constraints from real-world data. To improve the scalabil-ity of SMT(LRA) learning, we present a novel approach calledSHRECwhich uses hierarchical clustering to guide the search, thus reducing run-time. A designer can choose between higher quality (SHREC1) and lowerruntime (SHREC2) according to their needs. Our experiments show asignificant scalability improvement and only a negligible loss of accuracycompared to the current state-of-the-art.