=Paper=
{{Paper
|id=Vol-1163/paper-13
|storemode=property
|title=Towards Conflict-Driven Learning for Virtual Substitution
|pdfUrl=https://ceur-ws.org/Vol-1163/paper-13.pdf
|volume=Vol-1163
|dblpUrl=https://dblp.org/rec/conf/smt/KorovinKS14
}}
==Towards Conflict-Driven Learning for Virtual Substitution==
<pdf width="1500px">https://ceur-ws.org/Vol-1163/paper-13.pdf</pdf>
<pre>
Towards Conflict-Driven Learning for Virtual
                Substitution
         Konstantin Korovin1 , Marek Košta2 and Thomas Sturm2
                           1
                           The University of Manchester, UK
                                korovin@cs.man.ac.uk
           2
             Max-Planck-Institut für Informatik, 66123 Saarbrücken, Germany
                   mkosta@mpi-inf.mpg.de, sturm@mpi-inf.mpg.de

                                        Abstract
     We consider SMT-solving for linear real arithmetic. Inspired by related work for the
 Fourier–Motzkin method, we combine virtual substitution with learning strategies. For the
 first time, we present virtual substitution—including our learning strategies—as a formal
 calculus. We prove soundness and completeness for that calculus. Some standard linear
 programming benchmarks computed with an experimental implementation of our calculus
 show that the integration of learning techniques into virtual substitution gives rise to
 considerable speedups. Our implementation is open-source and freely available.

</pre>