Experiment design and administration for computer clusters for SAT-solvers (EDACC)

Abstract

The design of a SAT-solver or the modification of an existing one is always followed by a phase of intensive testing of the solver on a benchmark of instances. This task can be very time consuming even when using multi-core computers or computer clusters. To speed up this process we designed EDACC. A system capable of managing solvers with their parameters, instances, creating experiment jobs and running them on arbitrary multi-core systems. After loading solvers and instances into the system the user is able to configure the parameters of the solvers and choose the instances for the experiment and the settings of the runs. Then EDACC generates the jobs for the experiment and stores them in a database. The user only has to start the EDACC-clients on the target computing system. Each client will load jobs from the database and try to use the full computing capacity of the system to accomplish its tasks. The client will also monitor the resources of the solvers such as time and memory. When a job is finished the client will write the results back to the database and choose another job until all jobs are finished. The clients can be distributed on a grid to increase the throughput. System crashes will not affect the results because the results are saved to a remote database. The user only has to restart the client. With the help of this system, testing and comparing solvers can be done much faster and much more efficiently.