PSolver: Distributed SAT Solver Framework

PSolver is a framework for distributed SAT solving. Our goal is to take advantage of large numbers of idle networked machines to achieve speedups in the solution time of large SAT instances. The target environment is a large network, perhaps in a company or a research institutions, where large numbers or workstations are underused or idle for significant periods of time. Our architecture allows these workstations to devote some of their computing power to running a client that solves portions of SAT instances. We are using a master-slave topography whereby a server maintains a list of SAT instances to be solved, doles out portions of them to be solved by clients which connect and disconnect asynchroniously, and aggregates their results. Some important features of our system include:

• Solver-independent: Any single-process SAT solver (i.e. RELSAT, GRASP, SATZ, etc) can, with minimal effort, be plugged and used at the client end.
• Scalability: Our system is designed to be highly scalable. In the next release it will also support a high degree of hierarchization, meaning that a network can run a bunch of clients and a server which in turn acts as a client to a higher-level network. This will allow building very large clusters devoted to solving very large SAT instances.
• Voluntary Computing Environment Model: This implies support for asynchroniously connecting and disconnecting clients, as well as clients that can be run once on their machines and then left alone and will locate and connect to servers as they become available without need further intervention.
• Fault tolerance: The system is very fault tolerant - crashing clients do not affect the server, and a crashing server does not cause its clients to crash - they will locate another server to connect to, or wait for the crashed server to come back up
• Hardware/OS independence: Our system does not require any special-purpose hardware or software. It runs on normal workstations. It is written in c++ and compiled using the GNU compiler tools. We have binary distributions for Solaris, Linux, and Windows (using the Cygwin POXIX compatibility library). We do not anticipate that porting to other systems would be a problem
• Save/Restore: Our system supports saving the state of its work on an instance and can later resume working on that instance without losing the progress it had made up to that point.
• Solution Enumeration: For an instance with multiple solutions, we support solution enumeration.

Download the software
Get the source code - Coming soon
Brief User Guide (more documentation will be available soon)

This work is being carried out in the Software Design group at MIT Lab for Computer Science by Daniel Kokotov, under the guidance of Prof. Daniel Jackson. Please send feedback to dakokes@mit.edu. This is a work in progress. Bug fixes, new releases, and further documentation will be available soon. Check back here for updates.