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,
- 2014-11-22; in: "Human-Inspired Computing and Its Applications - 13th Mexican International Conference on Artificial Intelligence, MICAI 2014",
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.