[Back]

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

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

http://dx.doi.org/10.1007/978-3-319-13647-9_39