Armin Biere, Ioan Dragan, Laura Kovacs, Andrei Voronkov,
"Experimenting with SAT Solvers in Vampire"
: Proc. 13th Mexican Intl. Conf. on Artificial Intelligence, Serie Lecture Notes in Computer Science (LNCS), Vol. 8856, Springer, Seite(n) 431-442, 2014
Experimenting with SAT Solvers in Vampire
Sprache des Titels:
Proc. 13th Mexican Intl. Conf. on Artificial Intelligence
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.