SATSolver

SAT-based Sudoku solver. Uses minisat and walksat.
Comprised of a basic implementation and some extended functionality as well.

Contributers:
Yuki Hayashi
Spencer Vatrt-Watts
Mohammed Abousaleh
Zane Li

Files:
README
Report
sud2sat.py
sat2sud.py
test_puzzles.txt
test_puzzles_script.py
top95.txt
top95_script.py
test_puzzles_script_walksat.py
top95_script_walksat.py

README This file describes the contents of every file in the repository. In addition to the general descriptions of files, the Readme also includes details about our files that help people understand and use the code. Group member names are written in this file.

Report The report contains the description of two programs sat2sud and sud2sat as well as results of our experiments. The results of our experiment are about 50 puzzles that were solved by our programs. In addition, we provided info about the running the puzzles, which includes the mean, median, variance, and standard deviation.

sud2sat.py This file is a python script that reads a unsolved Sudoku puzzle in a specified format in a txt file. This generated txt file will be used for the input to the miniSAT solver. To run the sud2sat: $ python sud2sat.py name_of_test_file.txt Afterwards, a txt file called "sud2satOutput" will be generated To run this txt with miniSAT: $ minsat name_of_test_file.txt name_of_output_file.txt

Note: only one sudoku puzzle can be run in the test file.

sat2sud.py This file is a python script that reads the output generated from miniSAT and converts the output back into a sudoku puzzle encoded as an 81 character string. Convert the output back to a sudoku: $ python sat2sud.py name_of_test_file_of_sudoku_in_CNF.txt

Note: the solved sudoku puzzle will be shown in a 9x9 grid in the terminal.

test_puzzles.txt This file contains 50 unsolved sudoku puzzles that come from https://projecteuler.net/project/resources/p096_sudoku.txt. These puzzles were used to test our solution and we documented the results of the tests.

test_puzzles_script.py This file is an executable that runs unsolved sudoku puzzles from test_puzzles.txt and writes the results from miniSAT and puzzle solutions to two files.

First Extended Task

The first extended task consisted of testing the solver on hard inputs from http://magictour.free.fr/top95.

top95.txt This txt file includes the hard inputs from http://magictour.free.fr/top95. This contents of the file will be run by top95_script.py.

top95_script.py This file is an executable similar to test_puzzles_script.py, in which the program runs unsolved puzzles from top95.txt and writes the results from miniSAT and puzzle solutions to two files.

Second Extended Task

The second extended task consisted of testing a different SAT-solver. For this task we chose to use walksat, available at https://www.cs.rochester.edu/u/kautz/walksat/. Walksat must be installed for the following script to work, this can be accomplished by running the makefile included in this repo.

test_puzzles_script_walksat.py This file is an executable that runs unsolved sudoku puzzles from test_puzzles.txt and writes the results from walksat and puzzle solutions to two files.

top95_script_walksat.py This file is an executable similar to test_puzzles_script_walksat.py, in which the program runs unsolved puzzles from top95.txt and writes the results from walksat and puzzle solutions to two files.