README file of SugarTracer

Table of Contents

Overview

This document describes the usage of SugarTracer program which can trace SAT solver's process working for a CNF file generated by Sugar.

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-0.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

Browser GUI

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

$ java -jar bin/sugartracer-v1-0-0.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.

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-0.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.

  1. Start the web server with the following command.
    $ java -jar bin/sugartracer-v1-0-0.jar -server html sample/sudoku-0.cnf sample/sudoku-0.map
    
  2. Open http://localhost:8080/html/sugartracer.html in your Web browser.
  3. Click "Step" button twice.
  4. Click "Col+" button four times to resize variables table to 9x9.
  5. 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!

License

This software is distributed under the BSD License.

Links

Date: 2012-11-30 22:39:56 JST

Author: Naoyuki Tamura

Validate XHTML 1.0