Overview
Many SAT instances arising out of real-world problems such as model-checking require hours, even days, to solve, in the process taking up significant system resources. It would be very useful to be able to have, at any point, a measure of the progress made on solving the instance so far. Unfortunately, no such facility currently exists for any of the major SAT solvers in use. Our progress bar attempts to fix this shortcoming.
In addition to providing a measure of progress towards the solution of a SAT instance, a progress bar for SAT solvers has another, potentially more important purpose: it can be used to achieve a better algorithm for solving SAT instances. There are several SAT solvers in use today; all use slightly different algorithms and heuristics; many also have several heuristics they can use. Though on average some solvers may outperform others, for any given instance it is very difficult to predict which solver will provide the optimum result. Moreover, the difference between the optimum and non-optimum solver can be quite large. If we could have a reasonably dependable progress bar, we could use it to select the optimum solver by running several solvers for a short time, choosing the one that made the most progress in that time, and running it on the whole problem. If the instance is sufficiently large, the overhead of running several servers for a short time initially is small compared to the savings achieved by using the optimal algorithm.
Results
We have written a paper describing in more detail the our algorithms and results. You can read it here in Postscript or PDF format.
Download the Software
Source code for the progress bar is available for download. We've compiled it on the Linux, Solaris, and Windows (with Cygwin) platforms using g++ without any problems.
There are three options for downloading the software:
Relsat/Progress Bar. This is the latest version of Relsat (2.00) instrumented with the progress bar. Get it here (tar-gzip).
Sato/Progress Bar. This is the latest version of Sato instrumented with the progress bar. Get it here (tar-gzip).
Standalone Progress Bar. If you're using a different solver you can download just the progress bar code and instrument your solver with it. Our paper explains how to do this. Download the standalone progress bar code here (tar-gzip).