Centre de Recherche en Informatique de Lens
université d'Artois cnrs

Dolius

Information

This page presents Dolius, a SAT solving framework. It is intended to be a generic tool to test different divide and conquer methodologies. It allows to:
  • Use workers to solve a SAT instance. A worker is a computing unit offering a slightly modified SAT solver, communicating with a master through TCP/IP.
  • Solve the SAT instance on a cloud
  • Use clauses to divide the work between workers
  • Send generated clauses to every worker
  • Add resources on the fly, when needed
  • Plug in any SAT solver that implements a given interface


Dolius is brought to you by:
  • Gilles Audemard, Professor at Université d'Artois, co-author of the award winning solver glucose
  • Saïd Jabbour, Assistant Professor at Université d'Artois, co-author of the award winning parallel solver manysat
  • Cédric Piette, Assistant Professor at Université d'Artois, co-author of the preprocessing technique ReVivAl
  • Benoît Hoessen, PhD Student at Université d'Artois, main developer on dolius and on the award winning parallel solver PeneLoPe

Related paper:
  • Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Cédric Piette, "Dolius: A Distributed Parallel SAT Solving Framework ". in Pragmatics of SAT 2014 (POS2014), July 2014.
  • Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Cédric Piette, "An Effective Distributed D&C Approach for the Satisfiability Problem". in 22nd International Conference on Parallel, Distributed and Network-Based Computing (PDP'14), February 2014.

Logs

When developing a platform as Dolius, tools must be provided to help the solver developer in understanding what is happening. Those logs can be helpful to fully understand what is happening in the master or in each worker. In order to facilitate the reading of those logs, a simple script has been written to provide some colors to the possible wall of text. A sample is provided below.

...
[2013/12/21 09h51m08s0688] Waiting for connection in queue
[2013/12/21 09h51m08s0695] #179 New connection: 127.0.0.1:50140
[2013/12/21 09h51m08s0696] #179 Treating connection 127.0.0.1:50140, idle
[2013/12/21 09h51m08s0696] #179 Obtained message: workRequest
[2013/12/21 09h51m08s0696] #179 Trying to contact 127.0.0.1:8044 to divide its work load to 127.0.0.1:8045 through connection #180
[2013/12/21 09h51m08s0697] Waiting for connection in queue
[2013/12/21 09h51m08s0697] #180 Treating connection 127.0.0.1:8044, waitingDivideConfirm
[2013/12/21 09h51m08s1698] #180 No confirmation yet from 127.0.0.1:8044
[2013/12/21 09h51m08s1698] Waiting for connection in queue
[2013/12/21 09h51m08s1698] #179 Treating connection 127.0.0.1:50140, waitingReady
[2013/12/21 09h51m08s2071] #179 Connection with 127.0.0.1:50140 is waiting for 127.0.0.1:8044
[2013/12/21 09h51m08s2071] Waiting for connection in queue
[2013/12/21 09h51m08s2071] #180 Treating connection 127.0.0.1:8044, waitingDivideConfirm
[2013/12/21 09h51m08s2071] #180 Received ack for division from 127.0.0.1:8044
[2013/12/21 09h51m08s2071] Waiting for connection in queue
[2013/12/21 09h51m08s2071] #180 Treating connection 127.0.0.1:8044, waitingReady
[2013/12/21 09h51m08s2072] #180 A slave is added: 127.0.0.1:8045, now 4 slaves
...
Eventhough logs are usefull, a visualization tool may provide some information in a much friendlier way. Therefore, we also made a small program that parses the logs of Dolius + GLUCOSE and produce a graph.
The following image represent the visualization of an execution using 4 workers. In each node, multiple informations are given:
  1. The IP and port of the worker
  2. The time work was done on that particular search space
  3. The time the worker had to wait before starting the search
  4. The interval when this node was active
  5. The shape of the node represent the state of the search: round unknown, octogon UNSAT and rectangle SAT
  6. The color of the node is red if the node was stopped due to a clause that led directly to a conflict
Edges between the nodes are colored accordig to the weight (in time) of the corresponding subtrees and are labeled using the variable that has been chosen for the division. ctl_4201_555_unsat.cnf
An archive containing the logs that were used to produce this tree is available here.

Animation
As the image is done through the scalable vector graphics technology, based on XML, a javascript was written in order to provide a basic animation of the tree. Controls are: left arrow to increment time of one second, left to decrement the time and spacebar will activate a popup showing the current time. Active nodes have their borders drawn, others don't. (Click on the image above to access the animation mode)


Evaluation

Results according to a increasing number of workers, using the implementation Dolius+Glucose
Dolius+GLUCOSE
In order to evaluate our work, different benches are used from the SAT Competition 2013. The method used to select those was the following: in order to be chosen, a bench:
  • needs to be solved by at least one of the first five parallel solver of the 2013 competition
  • may not be solved by each of the first five parallel solver of the 2013 competition
When that first selection was made, we tried to take different instances from different categories, with a high range for time needed by the best solver.


Implementing

Some kind of tutorial will be provided to ease the integration of solvers with dolius.


Sources

The sources of dolius will be available at bitbucket for July 2014.