SugarTracer

Overview
Download
Example Usage
- Open-Shop Scheduling (OSS)
- Sudoku
How to trace your CSP
- Remarks
Options
Known Bugs
Implementation
License
Links

Overview

This document describes the usage of SugarTracer program which can trace SAT solver's process working for a CNF file generated by Sugar (a SAT-based CSP solver). It shows trace information after decoding. Therefore, you can see the information at CSP level.

Example of Tracing Open-Shop Scheduling instance gp03-01

Download

sugartracer-v1-0-1.zip (version 1.0.1, released 2012-12-02 Sun)
The following files are also included.
- Class files of Sat4j
- Class files of JSON in Java
- Raphaël (JavaScript library for vector graphics)
sugartracer-v1-0-0.zip (version 1.0.0, released 2012-12-01 Sat, 1,863,453 bytes)

Example Usage

Open-Shop Scheduling (OSS)

Text output

The following command shows the trace of solving OSS instance gp03-01 by Guéret and Prins.

$ java -jar bin/sugartracer-v1-0-1.jar sample/gp03-01-sat.cnf sample/gp03-01-sat.map

var int makespan 1000..1168 undef
var int s_0_0 0..507 undef
.....
var bool q_1_2_2_2 undef undef
startSolver
decide makespan>1000
var int makespan 1001..1168 1000..1168
propagate makespan>1000
.....
conflict s_0_0>421 s_0_0<=422
backjump 2
var int makespan 1001..1168 1165..1168
.....
undo -q_0_2_2_2
learnt -q_0_0_0_2 s_2_1<=324 -q_1_1_1_2
var bool q_0_0_0_2 false undef
.....
found
sat
stopSolver

Web Browser GUI

The following command starts the web server for visualizing the trace on Web browser.

$ java -jar bin/sugartracer-v1-0-1.jar -server html sample/gp03-01-sat.cnf sample/gp03-01-sat.map

Then, open your Web broswer for http://localhost:8080/html/sugartracer.html, and click "Step" button to see stepwise trace.

Click "Quit" and "OK" to stop the server.

Web Browser GUI with Graphical Visualization

For gp03-01 instance, graphical visualization page is available.

Start the web server with the following command.

$ java -jar bin/sugartracer-v1-0-1.jar -server html sample/gp03-01-sat.cnf sample/gp03-01-sat.map

Open your Web broswer for http://localhost:8080/html/gp03-01.html, and click "Step" button to see stepwise trace.

Click "Quit" and "OK" to stop the server.

Sudoku

Sudoku is a famous puzzle invented by Nikoli. We use a puzzle explained in http://www.nikoli.co.jp/en/puzzles/sudoku.html.

Start the web server with the following command.

$ java -jar bin/sugartracer-v1-0-1.jar -server html sample/sudoku-0.cnf sample/sudoku-0.map

Open http://localhost:8080/html/sugartracer.html in your Web browser.
Click "Step" button twice.
Click "Col+" button four times to resize variables table to 9x9.
Click "Step" button to see how SAT solver solves this puzzle.

Note that only unit propagations are necessary to solve this puzzle. No decisions, no backtracks!

How to trace your CSP

Compile your CSP by Sugar to get CNF and Map files
```
$ sugar -n -sat file.cnf -map file.map file.csp
```
Run SugarTracer server
```
$ java -jar sugartracer-v1-0-1.jar -server sugartracer-v1-0-1/html file.cnf file.map
```
- sugartracer-v1-0-1/html should be a directory name containing sugartracer.html file.
Open http://localhost:8080/html/sugartracer.html in your Web browser.

Remarks

It is not practical to trace large CNF.
Use -quick option to speedup tracing.
Hiding "Console" (and others) also makes tracing faster.

Options

-server dir : Run SugarTracer as HTTP server
- dir is a directory name where sugartracer.html exists.
-port num : Port number of HTTP server (default 8080)
-quick : Faster response by ommiting 'propgate' and 'undo' information

Known Bugs

Sometimes "Restart" and "Quit" buttons do not work correctly…

Implementation

SAT solver level tracing informaiton is obtained by using SearchListener interface of Sat4j.
The information is decoded to CSP level by using the map file data generated by Sugar.
Ajax with JSON data format is adopted for the communcation between Web browser and HTTP server.
User interface part in the Web browser is implemented in JavaScript.
Raphaël is used to draw the diagram of gp03-01 OSS instance.
If you want to write tracer of your SAT solver, create your subclass of SatSolver implementing the followings.
- startSolver() method
- stopSolver() method
- restartSolver() method
- Call tracer.decide(lit) when deciding a literal
- Call tracer.propagate(lit) when propagating a literal
- Call tracer.undo(lit) when undoing a literal
- Call tracer.backjump(backjumpLevel) when backjumping
- Call tracer.conflict(clause) when the conflict is found at the clause
- Call tracer.learnt(clause) when the learnt clause is obtained
- Call tracer.found() when a solution is found
- Call tracer.restart() when restarting
- Call tracer.end(result) when the solver finished

License

This software is distributed under the BSD License.