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.


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.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence