A Multithreaded Vampire with Shared Persistent Grounding

Abstract

Automated theorem provers (ATPs) typically run in a single thread. Hardware parallelism is then exploited through portfolios, in which distinct and disjoint strategies are launched as fully-independent processes and do not cooperate. Whilst there has been some historic exploration of cooperation, the technical challenge has prevented this from being fully explored in modern ATPs. The following describes the non-trivial engineering effort required to make the Vampire theorem prover multithreaded, such that multiple proof attempts coexist in the same memory space. This lays the foundations for a new generation of proof search techniques able to cooperate with other proof attempts running in parallel. As an initial demonstration, we implement a shared persistent grounding daemon that receives all clauses generated by all proof attempts and checks whether a heuristically-grounded version is unsatisfiable. The resulting multi-threaded system achieves limited contention compared to the previous process-based implementation, and persistent grounding improves performance in certain cases.