SAT Over BOINC: An Application-Independent Volunteer Grid Project

BOINC is a well-known middleware application for distributing projects over a volunteer grid. Most popular BOINC projects are designed for a specific research problem. Lacking is a general-purpose project that allows researchers, with no experience with the BOINC API and little means of hosting a server, to dispatch their own parallel computations to the volunteer grid. This paper describes a BOINC boolean satisfiability (SAT) solver that accepts equations submitted by external contributers via a Python module or a web interface. It parallelizes the SAT equation, dispatches sub problems to volunteer clients, assembles the result, and returns it to the researcher. The solver is shown scale with the number of nodes, and outperforms serial SAT solvers, even with the BOINC overhead, for SAT equations of 40 variables or more. The project uses a flexible framework so that future solvers can be built with it.