[Back]

G. Reger, M. Suda:
"Incremental Solving with Vampire";
Talk: Fourth Vampire Workshop - VAMPIRE 2017, Gothenburg, Sweden; 2017-08-07.

Both SMT and SAT solvers can be used incrementally. This can be useful in lots of applications. Indeed, internally, Vampire uses both Minisat and z3 incrementally. In this paper, we explore how Vampire can be used incrementally. There are two forms of incremental solving. The first is where a solver is provided with formulas from a problem one by one with consistency being checked at certain points. The second more general form is where stack operations are used to create different solving contexts. We explore both ideas and show how they can be achieved within Vampire. We argue that the second approach may be more suited to Vampire as it allows for the incremental solving of unsatisfiable problems (whereas the first assumes a series of satisfiable problems) and the use of different solving contexts allows Vampire to make use of incomplete proof search strategies. For the first approach, it is necessary to restrict preprocessing steps to ensure completeness when additional formulas are added. For the second approach, we make use of clauses labelled with assertions and take advantage of AVATAR to keep track of the stack information.

theorem proving, Vampire, SMT solving

http://publik.tuwien.ac.at/files/publik_264640.pdf