Talks and Poster Presentations (with Proceedings-Entry):

A. Biere, I. Dragan, L. Kovacs, A. Voronkov:
"Experimenting with SAT Solvers in Vampire";
Talk: Lecture Notes in Computer Science, Mexico; 2014-11-16 - 2014-11-22; in: "Human-Inspired Computing and Its Applications - 13th Mexican International Conference on Artificial Intelligence, MICAI 2014", Mexico (2014), ISSN: 0302-9743; 431 - 442.

English abstract:
Recently, a new reasoning framework, called AVATAR, integrating first-order theorem proving with SAT solving has been proposed. In this paper, 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.

First-order theorem proving, SAT solving, AVATAR

"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)

Created from the Publication Database of the Vienna University of Technology.