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.
- 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
- 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!
License
This software is distributed under the BSD License.
Links
- Sugar
- Sat4j (SAT solver in Java)
SugarTrace uses Sat4j as interal SAT solver engine. - JSON in Java
- Raphaël (JavaScript library for vector graphics)