[Zurück]


Vorträge und Posterpräsentationen (ohne Tagungsband-Eintrag):

I. Dragan et al.:
"Experimenting with SAT Solvers in Vampire";
Vortrag: RiSE/Puma meeting, Mondsee; 29.09.2014 - 03.10.2014.



Kurzfassung englisch:
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

Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.