Distributed SAT solving—A case study in distributed theorem proving

Theorem proving is a computationally intensive task with huge search spaces and as such, is a natural application area for the paradigm of concurrent and distributed programming. The aim of this project has been to build a theorem proving framework that allows for concurrent, asynchronous interacting computational tasks at a fine level of granularity and thereby enabling tapping of the latent co-routing possibilities present within a theorem proving task, encoding of distributed patterns of reasoning, opening up fresh perspectives on the theorem proving task and providing more processing power. As a proof of concept, a distributed SAT solver based on the DPLL and Stalmarck algorithms has been implemented using Alice, a functional programming language based on Standard ML, extended with rich support for concurrent, distributed,and constraint programming. This talk will discuss this work on the distributed SAT solver, as a particular instance of distributed theorem proving. I will also present some ideas on ongoing work on building a distributed first-order prover.

(this is a 3rd year PhD project presentation)