To Örebro University

oru.seÖrebro University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Learning SMT(LRA) Constraints using SMT Solvers
Katholieke Universiteit Leuven, Leuven, Belgium.
Katholieke Universiteit Leuven, Leuven, Belgium.
University of Trento, Trento, Italy.
Katholieke Universiteit Leuven, Leuven, Belgium.ORCID iD: 0000-0002-6860-6303
2018 (English)In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, AAAI Press, 2018, p. 2333-2340Conference paper, Oral presentation with published abstract (Refereed)
Abstract [en]

We introduce the problem of learning SMT(LRA) constraints from data. SMT(LRA) extends propositional logic with (in)equalities between numerical variables. Many 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.

Place, publisher, year, edition, pages
AAAI Press, 2018. p. 2333-2340
Series
IJCAI International Joint Conference on Artificial Intelligence, ISSN 1045-0823
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:oru:diva-90769DOI: 10.24963/ijcai.2018/323ISI: 000764175402066Scopus ID: 2-s2.0-85055709771ISBN: 9780999241127 (print)OAI: oai:DiVA.org:oru-90769DiVA, id: diva2:1540312
Conference
27th International Joint Conference on Artificial Intelligence (IJCAI 2018), Stockholm, Sweden, July 13-19, 2018
Funder
EU, Horizon 2020, 694980Available from: 2021-03-29 Created: 2021-03-29 Last updated: 2025-01-20Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

De Raedt, Luc

Search in DiVA

By author/editor
De Raedt, Luc
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 52 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf