20-ECES-228-001 Data Structures Fall 2007

Homework Assignment Number 1

Sudoku Solver

Due: September 28, 2007
Submit source code for backtracker solver and logic modeller to xxxxx@email.uc.edu

Rationale:
    This is a warm-up for work we will be doing this quarter. There are numerous ways to solve a Sudoku puzzle and most find solutions quickly. In this homework we will attempt to solve a puzzle by means of backtracking and by transforming to logic constraints and solving with a SAT solver.

Purpose:
    Use classes in a meaningful way, to represent objects. Read input data from a file. Recall backtracking and recursion. Study transformation to logic constraints.

Background:
    The game of Sudoku is played on a 9x9 grid. The grid is divided into 9 3x3 subgrids, three across at the top, three across in the middle and 3 across at the bottom. At the start of a game some elements (about 30) have numbers and some (about 51) do not (that is, they are unassigned). A player must place numbers in unassigned elements. A game is completed and won by a player if the following constraints are satisfied:
  1. Each element of the grid contains a number from 1 to 9.
  2. The initial element values are unchanged by the player.
  3. There are no duplicate numbers among elements of each subgrid.
  4. There are no duplicate numbers among elements of any row.
  5. There are no duplicate numbers among elements of any column.
The following is a java implementation.

      

The numbers in dark squares are the initial element assignments. Click on Solve to attempt to complete a solution to the current assignment of numbers. Choose another initial set of numbers by clicking on the File button and selecting a file. Click on Clear to clear only the numbers in the lightly colored squares. Click on Clear All to clear the entire board. To set fixed numbers (dark squares), click on a square, enter a number, and then hit the "Enter" key. Erase by hitting the backspace key. If there is no solution to the problem at hand, numbers will not be shown in the lightly colored squares.

Backtracking and Recursion: The following is a general template for solving a problem by means of backtracking. The type of problem solved requires filling an array with values that do not violate constraints. Values are tried for each array elements consecutively. If constraints are not violated, a value is found for another element. If some constraint is violated another value is tried for the current array element. If all values have been tried for the current array element and none satisfy constraints then change the value of a previously assigned array element.

    Solve(d)
        /* Assume I is a global structure containing initial values. */
        /* V is a global array that will be filled with values by this procedure. */
        /* Assume V is initialized, if necessary. */
        /* d is the number of array elements that have not been set. */

        If d == 0 then output V;   /* All elements have values, constraints satisfied */
        For each possible value t for array element V[d]:
            V[d] = t;
            If constraints are satisfied by assigned elements of V then Solve(d-1);
        Unassign V[d];
        Return;

Logic modelling: problems may be modelled with 0-1 valued variables and binary logic operators including 'or' (∨), 'and' (∧), 'exclusive-or' (⊕), 'not' (¬), 'equivalent' (≡), among others. Logic expressions may consist of subexpressions which are delimited with parentheses. Evaluation of a logic expression is from innermost subexpression out. For example, consider the following logic expression:

v4≡ ((v1∨¬v2)∧ (v2∨¬v3)∧ (v3∨¬v1)).
This expression has 4 variables: v1, v2, v3, v4. If these variables are all assigned the value 1, the logic expression evaluates 1 to because (v1∨¬v2), (v2∨¬v3), and (v3∨¬v1) all evaluate to 1 so, substituting these values for the subexpressions, 1∧1∧1 evaluates to 1, and finally 1≡1 evaluates to 1. Once a problem is modelled with logic constraints, a logic solver may be applied to find an assignment of values that causes all constraints to evaluate to 1.

Analysis:
    We have to decide on a file format, an internal data representation, and finally how the constraints are to be implemented.

File Format: The simplest format is to have the file store 0s for unassigned elements, and numbers from 1-9 for the fixed elements. Since we will read these numbers consecutively, it is best to store them in row major order. Since we will want to edit input files without the use of special editing software, the file should be a straight text file. The following illustrates a perfectly fine format for our purposes:

   0 6 0  1 0 4  0 5 0
   0 0 8  3 0 5  6 0 0
   2 0 0  0 0 0  0 0 1

   8 0 0  4 0 7  0 0 6
   0 0 6  0 0 0  3 0 0
   7 0 0  9 0 1  0 0 4

   5 0 0  0 0 0  0 0 2
   0 0 7  2 0 6  9 0 0
   0 4 0  5 0 8  0 7 0
where we have put in some double spacing for readability.

Data Representation, Backtracking: The backtrack template above aims to fill array elements in order. Therefore, it is reasonable to represent all 81 board positions in an array of 81 elements. We interpret each array as follows: 0 means unassigned, 1-9 is a value that is for the corresponding board position. We can use the following C++ declaration to hold this array:

   int *board = new int[81];
Thus, board[10] is the second column (that is, column 0) in the second row (that is, row 1), board[24] is the seventh column (column 6) of the third row (row 2), and so on. Given an index into the array board we can find the corresponding row and column in C++ as follows:
   row = index/9;
   column = index%9;
Given a row and column the corresponding index into array board is
   index = 9*row + column;
We aim to use both conversions because it is easier for the solver to have the data stored as an array and easier to implement constraints in terms of rows and columns.

Data Representation, Logic: Many more variables are needed here than for backtracking since each variable can only take values 0 and 1. For the ith row and jth column we can use another 9 variables. The total number of variables will then be 9*81 = 729. Number the elements of each of the 3x3 subgrids as follows:

   0 1 2
   3 4 5
   6 7 8
Give each subgrid an identity as follows:
   0 1 2
   3 4 5
   6 7 8
For purposes of discussion let's identify each variable with three parameters and intended meaning as follows:
   w[i,j,k] = 1  if the value of the jth element of the ith subgrid has value k 
   w[i,j,k] = 0  otherwise
As for the case of the backtracking representation we will use an array board to store all these variables. The conversion from i,j,k to array index is given by
   index = 81*i + 9*j + k
The conversion from index to i,j,k is as follows
   i = ((index-1)/81)%9;
   j = ((index-1)/9)%9;
   k = (index-1)%9;
We will also have to worry about the output format because the result of the logic program will be to generate a file that will serve as input to a Satisfiability solver. The format we need is exemplified by the following:
   p cnf 729 10317
   1 2 3 4 5 6 7 8 9 0
   10 11 12 13 14 15 16 17 18 0
   19 20 21 22 23 24 25 26 27 0
   28 29 30 31 32 33 34 35 36 0
   37 38 39 40 41 42 43 44 45 0
   46 47 48 49 50 51 52 53 54 0
   55 56 57 58 59 60 61 62 63 0
   64 65 66 67 68 69 70 71 72 0
   ...
   -3 -4 0
   -3 -5 0
   -3 -6 0
   -3 -7 0
   -3 -8 0
   -3 -9 0
   -4 -5 0
   -4 -6 0
   -4 -7 0
   -4 -8 0
   -4 -9 0
   ...
where the first line always begins with "p cnf" and has parameters which are the number of variables (729 in this case) and the number of constraints (10317 in this case). The constraints all follow the first line and are expressed one constraint per line of file. All but about 30 of the constraints are the same for all problems as will be discussed later. The ones that are fixed will be given to you. Hence all you have to do is append the 30 or so constraints that represent the particular puzzle you are trying to solve and change the 10317 accordingly. Each constraint ends in 0 - that tells the solver that there are no more variables in the constraint. The numbers in the constraints are the indices into the board array, plus 1 (0 is not allowed because it is a terminating character). If a '-' preceeds a number that means the variable is negated.

Constraints, Backtracking: Each of 9 subgrids has to be checked to make sure all assigned values are distinct. For each subgrid there should be two nested for loops to traverse all rows and columns like this:

   for (int r=imin ; r < imin+3 ; r++) {
      for (int c=jmin ; c < jmin+3 ; c++) {
where imin and jmin are the starting row and column numbers for the subgrid. For example, the upper left subgrid starts at imin=0 and jmin=0. Assign a counter to each number from 1 to 9. Initialize each counter to 0. As each of 9 elements is considered increment the counter associated with the value of the element. If any count goes past 1, there is a violation and backtrack must commence.

Each of 9 rows must be checked similarly. This time there is just one for loop, spanning all the rows of a particular column. Assign counters as before to the numbers from 1-9 and increment as those number are encountered in the loop.

Repeat the above for columns. The code is nearly the same.

Constraints, Logic: The 10287 fixed constraints, which comply with the conversions between i,j,k and w array index as stated above, are given in the file sudoku.cnf. These constraints are all logical 'or' subexpressions. Since they are given in the file you do not have to construct them yourself. But the interested reader may look at this page to see how they are constructed. You need to append to that file one constraint for every fixed number that is expressed in the input file. For example, if the 0th element of the 2th subgrid has fixed value 4 we need to fix the value of board[2*81+0*9+4] to 1. The constraint added to the output file is:

   167 0
Remember to also calculate the number of constraints and prepend the header to the output file as well.

Homework Poblem:

    Write a Sudoku solver that is based on backtracking. The solver takes a file name as input. The file contains all the fixed numbers for a given puzzle. File details are given below. The solver outputs to console the solution to the given puzzle. Output details are given below. Write a logic modeller that takes the same file as input and outputs a file that may be solved by a SAT solver. Format of the output file is given above. You are welcome to try your output files on a SAT solver such as this one.

Requirements:

  1. Functional requirements (Input file format and output spec):
    1. Your program will read a text (input) file and display the results to the console. In the case of the logic output file, the console display may be redirected to a file by means of the '>' on the command line (even true for Windows!).
    2. The input file will be identified on the command line (that is, use int main(int argc, char **argv) - follow this link for examples).
    3. The input file will contain printable ascii characters only plus newline characters for terminating a line.
    4. The layout of the input file will resemble a Sudoku puzzle board. The input file will consist of 9 lines containing data. Blank lines between data lines will be allowed. Each line contains 9 blank separated digits. A digit between 1-9 in a position means a fixed number has been assigned to that Sudoku puzzle position - the output must preserve all fixed numbers. A sample input file is here.
    5. The output of the backtracking solver will consist of a 9x9 matrix of digits representing a solution to the given puzzle. An example of such an output is given here. The output is written to console.
    6. The output of the logic modeller is a header followed by a list of constraints. The header begins with "p cnf" and then contains the number of variables in the remainder of the file and the number of constraints. The constraints are lists of variable numbers, terminated with 0. Numbers may be preceeded by '-' indicating the corresponding variable is negated. A sample output file is given here.

  2. Performance requirements:
    1. Time: Less than 0.1 seconds to read an input file. Less than 1 second to solve a puzzle or to model one for a SAT solver. To determine how much time is used in each phase of a program use clock. For example, consider file tst.cc containing the following c++ source:
         #include <time.h>           // Be sure to include this header
         #include <iostream>
         using namespace std;
      
         int main () {
            clock_t t1 = clock();    // absolute time in microseconds
            for (int i=0 ; i < 1000000; i++);
            clock_t t2 = clock();    // absolute time in microseconds
            for (int i=0 ; i < 10000000; i++);
            clock_t t3 = clock();    // absolute time in microseconds
            cout << "Time: 1st loop=" << (t2-t1) << ", 2nd loop=" << (t3-t2) << "\n";
         }
      
      Compile using g++ tst.cc -o tst then run using ./tst. The output might look something like this
         Time: 1st loop=10000, 2nd loop=80000
      
      which means 0.01 seconds for the first loop and 0.08 seconds for the second loop.
    2. Space: Less than 2MB of RAM. To find how much space a program uses at a particular point use getchar() to pause the program then use ps v from the command line to see the space used. For example, consider file tst.cc containing the following c++ source:
         #include <iostream>
         using namespace std;
      
         int main () {
            getchar();
            int *a = new int[250000];
            getchar();
         }
      
      Compile this using g++ tst.cc -o tst. Then run it from the command line using ./tst. Open another shell and execute ps v | grep tst. You will see something like this:
         4865 pts/4    S+     0:00      0     2  7085   848  0.1 tst
         4872 pts/6    S+     0:00      0    80 56695   620  0.0 grep tst
      
      The first line shows the resources used by tst. The column showing 848 displays memory in residence used (in KB) and the column showing 7085 displays virtual memory used (in KB). The total used for our purposes will be the sum of the two. In the first shell hit return (advancing to the next getchar()) and in the second shell type ps v | grep tst again. You might see something like this:
         4865 pts/4    S+     0:00      0     2  8065   896  0.1 tst
         4877 pts/6    S+     0:00      0    80 56695   620  0.0 grep tst
      
      Observe that (8065+896)-(7085+848) = 1028 KB = 1003906 Bytes. Which is approximately the space added to the program by int *a = new int[250000]; since each int takes 4 bytes. The RAM usage we are looking for is the difference of the RAM used just before temination and the RAM used at entry. Hence a getchar() at the beginning and end of the program is enough to determine RAM.

  3. Implementation requirements:
    1. For the backtrack solver, use a Sudoku class to hold all data, read a file, solve a puzzle, and output results. Use the following prototype:
         class Sudoku {
            int *board;  // Board values
      		
         public:
            Sudoku () {            // Constructor
               board = new int[81];
               for (int i=0 ; i < 81 ; i++) board[i] = 0;
            }
      			
            void readFile (char *filename) {
               ...
            }							 
      
            // Pretty print number in row i, column j of the board
            void printCell(int i, int j) {  ... }
      							
            // Pretty print the entire board
            void printBoard () { ... }
      			
            // A number has just been placed in row i, column j.  If all columns
            // rows and squares do not violate contraints then return true, otherwise
            // return false.
      	   bool check (int i, int j) {
               int count[9];  // To determine whether there is a violation
               for (int i=0 ; i < 9 ; i++) count[i] = 0;
      		
               // Check small square
               ...
      						       
               // Check row
               ...
      
               // Check column
               ...
            }
      
            void solve (int d) { ... }
         }
      

    2. The above can be used in main as follows:

         int main (int argc, char **argv) {
            if (argc != 2) {
               cerr << "Usage: " << argv[0] << " \n";
               exit(0);
            }
      						
            Sudoku *game = new Sudoku();
            game->readFile(argv[1]);
            game->solve(81);
            game->printBoard();
         }