Clustering-guided SMT(LRA) learning

Tim Meywerk; Marcel Walter; Daniel Große; Rolf Drechsler

Clustering-guided SMT(LRA) learning

Tim Meywerk
, Marcel Walter
, Daniel Große
, Rolf Drechsler

Institute of Complex Systems

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

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.

Original language	English
Title of host publication	International Conference on integrated Formal Methods (iFM)
Number of pages	18
Publication status	Published - 2020

Fields of science

202005 Computer architecture
202017 Embedded systems
102 Computer Sciences
102005 Computer aided design (CAD)
102011 Formal languages

JKU Focus areas

Sustainable Development: Responsible Technologies and Management

Cite this

@inproceedings{44abebb23c194fdda4c16fc21cab72d6,

title = "Clustering-guided SMT(LRA) learning",

abstract = "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.",

author = "Tim Meywerk and Marcel Walter and Daniel Gro{\ss}e and Rolf Drechsler",

year = "2020",

language = "English",

booktitle = "International Conference on integrated Formal Methods (iFM)",

}

TY - GEN

T1 - Clustering-guided SMT(LRA) learning

AU - Meywerk, Tim

AU - Walter, Marcel

AU - Große, Daniel

AU - Drechsler, Rolf

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

M3 - Conference proceedings

BT - International Conference on integrated Formal Methods (iFM)

ER -