SAT solving experiments in Vampire

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.