{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,26]],"date-time":"2026-01-26T15:58:15Z","timestamp":1769443095952,"version":"3.49.0"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,7]]},"abstract":"<jats:p>We introduce the problem of learning SMT(LRA) constraints from data. SMT(LRA) extends propositional logic with (in)equalities between numerical variables.\n\nMany 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.<\/jats:p>","DOI":"10.24963\/ijcai.2018\/323","type":"proceedings-article","created":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T05:49:10Z","timestamp":1530769750000},"page":"2333-2340","source":"Crossref","is-referenced-by-count":20,"title":["Learning SMT(LRA) Constraints using SMT Solvers"],"prefix":"10.24963","author":[{"given":"Samuel","family":"Kolb","sequence":"first","affiliation":[{"name":"KU Leuven"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Teso","sequence":"additional","affiliation":[{"name":"KU Leuven"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Passerini","sequence":"additional","affiliation":[{"name":"University of Trento"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luc","family":"De Raedt","sequence":"additional","affiliation":[{"name":"KU Leuven"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"name":"Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}","theme":"Artificial Intelligence","location":"Stockholm, Sweden","acronym":"IJCAI-2018","number":"27","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)"],"start":{"date-parts":[[2018,7,13]]},"end":{"date-parts":[[2018,7,19]]}},"container-title":["Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T05:51:42Z","timestamp":1530769902000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2018\/323"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2018\/323","relation":{},"subject":[],"published":{"date-parts":[[2018,7]]}}}