Lemma Learning in SMT on Linear Constraints

DOI10.1007/11814948_17MaRDI QIDQ5756582zbMATH OpenOpenAlexFDO

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

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)

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

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

Describes a project that uses

Uses Software

• Chaff
• SIMPLIFY
• QOCA

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)