Lemma Learning in SMT on Linear Constraints

DOI10.1007/11814948_17zbMATH Open1187.68418OpenAlexW1539597483MaRDI QIDQ5756582FDOQ5756582

Authors: Yinlei Yu, Sharad Malik 

Publication date: 4 September 2007

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11814948_17

Recommendations

• Lemma Learning in the Model Evolution Calculus
• Learning general constraints in CSP
• Learning General Constraints in CSP
• Learning-assisted theorem proving with millions of lemmas
• scientific article; zbMATH DE number 1223545
• scientific article; zbMATH DE number 522871
• Constraint solving for finite model finding in SMT solvers
• Exact learning: on the boundary between Horn and CNF
• Induction for SMT solvers

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cited In (4)

• ASP modulo CSP: the clingcon system
• Efficient Term-ITE Conversion for Satisfiability Modulo Theories
• Towards conflict-driven learning for virtual substitution
• Local Search for SMT on Linear Integer Arithmetic

Uses Software

• QOCA
• SIMPLIFY
• Chaff

This page was built for publication: Lemma Learning in SMT on Linear Constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756582)