Description

In this homework, you will use a SAT solver to solve Sudoku.

• Read a Sudoku puzzle from the input
• Encode into CNF
• Use MiniSat to find an assignment to CNF (if satisfiable)
• Output solution from the assignment
• Or print “NO” (if the puzzle is not solvable)

2.Input / Output

Each input file contains a puzzle that

• has a size 𝑁Í𝑁, and
• is prefilled with numbers 0 to 𝑁, where 0 represents the square is empty.

3.Command line

Your Sudoku solver should take three arguments:

./solver [Input Puzzle Filename] [Output Puzzle Filename] [MiniSatExe] where MiniSatExe is the filename of the MiniSat executable.        

Practice/Real-Life Applications of Computational Algorithms – Homework 1

4. Hand in your assignment

Please upload the following files in a zip, specifying your ID (e.g., Student_ID.zip) to E3 by the deadline.

• Source code
• A report that introduces your implementation

5. Platform Linux