Talks and Poster Presentations (without Proceedings-Entry):
I. Dragan et al.:
"Experimenting with SAT Solvers in Vampire";
Talk: RiSE/Puma meeting,
Recently, a new reasoning framework, called AVATAR, integrating first-order theorem
proving with SAT solving has been proposed.In this talk, we experimentally analyze
the behavior of various SAT solvers within first-order proving. For doing so, we first
integrate the Lingeling SAT solver within the first-order theorem prover Vampire and
compare the behavior of such an integration with Vampire using a less efficient SAT
solver. Interestingly, our experiments on first-order problems show that using the best
SAT solvers within AVATAR does not always give best performance. There are some
problems that could be solved only by using a less efficient SAT solver than Lingeling.
However, the integration of Lingeling with Vampire turned out to be the best when it
came to solving most of the hard problems
Created from the Publication Database of the Vienna University of Technology.