Proposal

Summary

We are going to use OpenMP to create a fast parallel Sudoku solver using two different algorithms, Crooks algorithm and SAT solving. Crooks algorithm is a sudoku specific implementation. Sudokus are known to have an equivalent mapping to sat formula, so we plan to make a sat solver that will be pipelined to solve sudoku formulas.

Background

Sudoku is a puzzle in which an N^2x N^2 board must be filled with N^2 numbers each of 1 through N^2 such that each row, column, and NxN box only contains each number once. Traditional Sudoku boards are 9x9. Solving a Sudoku puzzle is an NP-hard problem, meaning there is no known polynomial time solution. This makes Sudoku a great problem for parallelization. The brute force solution is an effective way to solve the puzzle because it will always find a solution. There is a lot of potential for parallelization, as there are a lot of independent regions that need to be filled.

The Challenge

We are planning to implement two parallel Sudoku solving algorithms: one that is a human-like approach that trims the number of possibilities before brute forcing (known as Crook’s algorithm), and another that is a Sat solver. The human-like approach will be challenging because there are a lot of repeated computations, and we may waste time recalculating possible numbers for the same parts of the board. In addition, the sequential brute force solver is already quite fast so it could be difficult to achieve significant speedup.

The brute force, simple approach for sat solving is to do a depth first search through the solution space, where each node is a possible decision point for deciding a single literal to be True or False. We can think of any path through the decision tree that has not reached a leaf node to be a partial assignment of the sat formula. There are a few sequential optimizations that can be made for sat solving, including the pure literal rule (seeing if any of the literals appear in only one polarity) and unit propagation (seeing if any clauses have all false literals except for one undecided). The challenge will be to make a parallel approach using the same depth first search algorithm at its core that doesn’t waste the benefits of partial assignments eliminating large sections of the solution space with the same prefix as the partial assignment.

Resources

We plan to start from scratch and use the following resources as guidelines:

We will be running our Sudoku solving algorithms on the Xeon Phi.

Goals and Deliverables

We plan to start by implementing serial versions of both algorithms. Then we will implement parallel versions using OpenMP and run them on the Xeon Phi. We plan to implement several improvements in the Cook’s algorithm parallel version, including fixing numbers that can only go in one square. We plan on timing the end to end pipeline of parsing the sudoku, generating a sat formula, solving the sat formula, and constructing the completed sudoku puzzle for the sat algorithm. We will show plots of speedup and timing statistics.

Platform Choice

We plan to use OpenMP, as it provides a convenient way to parallelize loops. We will run our algorithms on the Xeon Phi.

Schedule

November 12: start implementing and testing serial algorithms

November 19: finish implementing and testing serial algorithms

November 26: continue implementing parallel solvers

December 3: test and run parallel solvers

December 10: make speedup graphs, poster, writeup, and prepare presentation