Towards conflict-driven learning for virtual substitution

DOI10.1007/978-3-319-10515-4_19MaRDI QIDQ2879330zbMATH OpenOpenAlexFDO

Authors Konstantin Korovin, Marek Koša, Thomas Sturm

Publication date 8 September 2014

Published in Computer Algebra in Scientific Computing (Search for Journal in Brave)

Full work available at URL http://ceur-ws.org/Vol-1163/paper-13.pdf

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Symbolic computation and algebraic computation (68W30)

Recommendations

• Virtual substitution for SMT-solving
• Lemma Learning in SMT on Linear Constraints
• Thirty years of virtual substitution. Foundations, techniques, applications
• A practical approach to satisfiability modulo linear integer arithmetic
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures

Cited in

(7)

• The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Virtual substitution for SMT-solving
• Thirty years of virtual substitution. Foundations, techniques, applications
• The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• FMplex: a novel method for solving linear real arithmetic problems
• FMplex: exploring a bridge between Fourier-Motzkin and simplex
• VIRAS: conflict-driven quantifier elimination for integer-real arithmetic

Describes a project that uses

Uses Software

• REDLOG

This page was built for publication: Towards conflict-driven learning for virtual substitution

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