Download PDFOpen PDF in browser

A Multithreaded Vampire with Shared Persistent Grounding

EasyChair Preprint no. 5855

5 pagesDate: June 23, 2021

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:5855,
  author = {Michael Rawson and Giles Reger},
  title = {A Multithreaded Vampire with Shared Persistent Grounding},
  howpublished = {EasyChair Preprint no. 5855},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser