GridSAT: a system for solving satisfiability problems using a computational grid

In this paper, we present GridSAT – a distributed and high performance complete satisfiability solver – and its application to a set of complex and previously unsolved satisfiability problems. Based on the sequential Chaff [M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver. Proceedings of the 38th Design Automation Conference (DAC2001), Las Vegas, June 2001] algorithm, we combine new distributed clause “learning” techniques with an efficient and autonomous grid implementation both to speed the time to solution and to solve problems too complex for other general solvers. By automatically adapting to changes in the availability of machines and carefully distributing the clause database, we show how GridSAT has been able to use, continuously, a diverse and dynamically changing resource pool to solve previously unsolved problems from the SAT 2002 [SAT 2002 Competition. http://www.satlive.org/SATCompetition/] and the SAT 2003 [SAT 2003 Competition. http://satlive.org/SATCompetition/2003/] competitions. We describe our enhancements to the Chaff learning algorithm that have enabled an efficient distributed implementation, and detail the technological approach we have taken to realizing this implementation.