GridSAT is a parallel and complete boolean satisfiability solver used to solve non-trivial SAT problems in a grid environment.  The application uses a parallel solver algorithm based on Chaff to (attempt to) solve SAT problems of the form 'given a large, non-trivial Boolean expression, is there a variable configuration (and what are the variable values) which results in the expression evaluating to TRUE?'  The system stands apart from other SAT solvers in the sense that it was designed explicitly to run in grid environments, and has built in intelligent parallelism scheduling mechanisms.  As a result of this design, the system has been used to successfully and quickly solve several previously unknown problems by utilizing vast amounts of computational resources.

The fundamental algorithm of GridSAT is a parallelization of the Chaff SAT solver, a highly optimized complete sequential solver based on the Davis-Putnam-Logeman-Loveland (DPLL) algorithm with many heuristic optimizations. GridSAT modifies Chaff to make it possible to divide the search space between many clients using a "decision" stack to keep track of progress. The initial decision stack contains only variable assignments that are definite. GridSAT proceeds by heuristically selecting a variable and a Boolean value to assign to it and adding this tentative "decision" (and any inferences that it enables) to the stack.  The program backtracks when conflicts are found, and eventually returns the assignment (if one is found) or failure (if all possibilities are exhausted). A major improvement to the DPLL algorithm is "learning", which enables the algorithm to deduce new clauses and store them in a local database. The new clauses are generated after a conflict and are used in backtracking.  A key to GridSAT's success is integrating these learning heuristics with runtime information about the status of the Grid. In particular, it attempts to split the program onto additional resources (i.e. assigning sub-problems to other Grid nodes) only when needed since the problem is tightly coupled. GridSAT splits the problem if memory is exhausted on a node, choosing the best available resources and tailoring the split itself to make the best use of those resources. The splitting mechanism also allows nodes to exchange the learned clauses.

GridSAT represents a grid application with resource requirements that are substantially different from our usual workflow tests.  Since it was designed as a grid program from first principles (rather than as an adaptation of a parallel implementation) it includes many fault tolerance, latency tolerance, and resource-aware scheduling features that are necessary for grid application performance as explicit structural components.  Thus, while it is code of some complexity, it represents the "high end" of grid application development as evidenced by its performance.

As a VGrADS driving application, GridSAT motivates both the functionality and the performance of the virtualized resource discovery and allocation mechanisms.  The GridSAT scheduler considers resources abstractly, strictly in terms of their performance characteristics.  This strategy, of course, is a good match with the VGrADS virtual grid (VG) mechanism. VGs will be used to replace the GridSAT-internal abstraction mechanisms as a test of both their functionality (GridSAT should continue to function correctly) and their performance (the native GridSAT implementation is a “base” case).  Moreover, GridSAT does not take advantage of virtualization in its native form.  The virtualization features of VGrADS will enable GridSAT to scale beyond its current capabilities (currently thousands of processors), which again, forms the basis of an important empirical test of the VGrADS prototypes.

Finally, GridSAT's resource usage model is substantially more dynamic than that of the other VGrADS driving applications.  It acquires resources only when it determines they will benefit execution (as opposed to having a maximal set specified when it is launched) and releases them as quickly as possible to prevent waste and promote allocation stability.  To do so, the valuation of resources at any given moment in a GridSAT execution is related to the resources GridSAT is currently holding.  This incremental form of resource discovery in which the currently held resources parameterize the resource search is unique among the VGrADS test codes, and motivates many of the dynamic features in the Virtual Grid Execution System (vgES) design.