A Multithreaded Vampire with Shared Persistent Grounding

EasyChair Preprint 5855

Abstract

Automated theorem provers (ATPs) typically run in a single thread with any parallelism being through portfolios where distinct and disjoint strategies are run in parallel. Whilst there has been some historic exploration of cooperation, the technical engineering challenge has prevented this from being fully explored in modern ATPs. This paper describes the (non-trivial) engineering efforts involved in making the Vampire theorem prover multi-threaded such that multiple proof attempts can co-exist in the same memory space. This lays the foundations for a new generation of proof search techniques able to utilise fine-grained cooperation between separate proof attempts. 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 (extended) multi-threaded framework achieves introduces limited contention compared to the previous process-based solution and persistent grounding improves performance in certain cases.

Keyphrases: Proof attempt, SAT solver, Thread Local Storage, automated theorem proving, clause splitting, data race, first-order, first-order logic, first-order theorem prover, grounding mechanism, parallel theorem proving, persistent grounding, proof search, saturation-based theorem prover, shared memory, shared persistent grounding, theorem prover, thread local

@booklet{EasyChair:5855,
  author    = {Michael Rawson and Giles Reger},
  title     = {A Multithreaded Vampire with Shared Persistent Grounding},
  howpublished = {EasyChair Preprint 5855},
  year      = {EasyChair, 2021}}