CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Experimenting with SAT solvers in vampire

A. Biere ; I. Dragan ; Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; A. Voronkov
Lecture Notes in Computer Science: Human-Inspired Computing and Its Applications. 13th Mexican International Conference on Artificial Intelligence, MICAI 2014, Tuxtla Gutiérrez, Mexico, November 16-22, 2014. Proceedings, Part I (0302-9743). Vol. 8856 (2014), p. 431-442.
[Konferensbidrag, refereegranskat]

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 firstorder 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.

Denna post skapades 2015-05-06. Senast ändrad 2015-07-28.
CPL Pubid: 216648


Läs direkt!

Länk till annan sajt (kan kräva inloggning)