The Uses of SAT Solvers in Vampire
Giles Reger, Martin Suda · EPiC series in computing · 2018
Reasoning in a saturation-based first-order theorem prover is generally expensive involving complex term-indexing data structures and inferences such as subsumption resolution whose (worst case) running time is exponential in the length of the clause. In contrast, SAT solvers are very cheap, being able to solve large problems quickly and with relatively little memory overhead. Consequently, utilising this cheap power within Vampire to carry out certain tasks has proven highly successful. We give an overview of the different ways that SAT solvers are utilised within Vampire and discuss further ways in which this usage could be extended