[Back]

I. Dragan et al.:
"SAT solving experiments in Vampire";
Talk: Vienna Summer of Logic - Vampire Workshop, Vienna; 2014-07-22 - 2014-07-23.

In order to better understand how well an external SAT solver would behave in the framework of a first order automated theorem prover we have decided to integrate in Vampire one of the best performing solvers available on the market, Lingeling. Although the process of integration is straight forward, by simply implementing some interfaces in order to make the two tools communicate and putting them together, there are a few problems that have to be overcome.

In this talk we are going to address both the issues that arise from integration of the two solver and present initial results obtained by using this combination. And also details about different strategies that are currently implemented.