SAT4J on the GRID

A first version of a distributed version of SAT4J based on the ProActive Framework, called "miniactive" was developped by Frédéric Fontaine during the second quarter of 2004. That version of SAT4J allows a user to distribute the computation needed for solving one SAT benchmark on a grid of computers (on a cluster or across the internet).

The latest version of the miniactive distributed solver is available on demand.

The good point of that work is that once the ProActive configuration file that setup the computers to be used is done, the command line interface is exactly the same as the local version of the solver.

However, that version has some efficiency issues :

The solver needs to create a new JVM on each node of the grid before distributing the work: this is very time consuming.
It is not possible for the moment to stop/reuse a solver on a node.
Workload balancing is NOT implemented
Some of the methods in the SAT4J library are throwing exceptions. Those methods cannot be distributed with ProActive.

We prefer sorting out those problems before making miniactive available on the web.

This work is a joint ongoing effort with the OASIS team in Nice, Sophia-Antipolis.