Project Sudoku


IMPLEMENTATION OF A SUDOKU LOGIC SOLVER BASED ON MBDD+CRD 

HISTORY

This was a project used in 2005, 2006, and 2007 for the class 
of FORMAL MODELING AND VERIFICATION at National Taiwan University. 
It is now used as an example for the utlization of REDLIB.  

GOAL 

Fill in the details of the main processing body in the do-loop 
of procedure main() in file sudoko.c so that procedure main() 
can solve sudoko puzzles correctly with REDLIB.  
Any implementation that does not rely on the symbolic reasoning facilities 
of REDLIB will be unacceptable and declined. 


INPUT FORMAT 

The input format is a 9 by 9 matrix in a file. 
For example, we may have the following input matrix in a file. 

806049205
090000304
400230000
100402059
605000408
240805007
000058002
507000080
908720501

A zero in an entry means that the value of that entry is not filled in 
in the input configuration.  
A non-zero value in an entry specifies the input value of that entry.  


INSTRUCTION ON REDLIB UTILIZATION

The whole thing runs in Linux.  
To run the program, just type `sudoko' followed by the input file name, 
say `board,' and you get the printout. 
Note that you have to include the path name in your rc file.  
Otherwise, you have to type in './sudoko board' to specify 
the current directory as the pathname.  

1. The data structures involved are the following.  

   Type red_type for nodes in MBDD+CRD.  
   
    
2. Basic data environment is as follows. 

   Array s[0..8][0..8] that record the 81 variable names of MBDD+CRD used 
   in the main processing body. 
   
   
3. Basic library procedure is as follows. 

  red_true() that returns the canonical representation of TRUE in MBDD+CRD. 
  
  red_false() that returns the canonical representation of FALSE in MBDD+CRD. 
    When you find out that sol has become RED_false(), it means there is 
    no solution (assuming your code is correct).
  
  red_diagram(format, a1, a2, ...) that returns a MBDD+CRD 
    for the formula of string format with arguments 
    substituted with a1, a2, ...
    The format string follows the style of printf(format, a1, a2, ...).   

  red_and(d1, d2) that returns the MBDD+CRD for the conjunction of 
  MBDD+CRDs d1 and d2. 
  
  red_or(d1, d2) that returns the MBDD+CRD for the disjunction of 
  MBDD+CRDs d1 and d2. 
  
  red_not(d) that returns the MBDD+CRD for the complement (negation) of 
  MBDD+CRD d. 
  
  red_first_cube(d) that returns the first cube (root-to-leaf path) in d. 
  
  red_next_cube(d) that returns the next cube (root-to-leaf) in d. 
  
  red_diagram_discrete_model_count(d) that returns the number of 
  discrete models (satisfying interpretations/valuations) in d. 

  red_begin_session(system_type, session_name, process_count) that 
  starts a REDLIB session. 
  
  red_end_session() that ends a REDLIB session. 
  
  red_begin_declaration() that starts the declaration of variables, 
  parameters, operation modes (control locations), transition rules, 
  and initial conditions. 
  
  red_end_declaration() that ends the declaration.  
  
  red_declare_variable(vtype, vname, lb, ub) that declares a global 
  variable of type 'vtype' and name 'vname'.  
  If it is of type RED_TYPE_DISCRETE, 'lb' and 'ub' is the 
  lower-bound and upper-bound of the variable values respectively. 

  red_garbage_collect(RED_GARBAGE_SILENT) that starts reclaim memory 
  used by the diagrams.  Note that REDLIB at this moment does not 
  do garbage-collection automatically and implicitly.  
  Users have to do it explicitly with this procedure. 
  
  red_push(d) that saves diagram d in the user stack so that it will 
  not be reclaimed in subsequent garbage collection.  
  Note that any other diagrams that are not saved in the user stack 
  are subject to the possibility of memory reclamation.  
  This procedure returns the index to the stack top. 
  This index may later be used for referencing and modifying values.  
  
  red_pop(int h) that pops the topmost frame from the user stack. 
  Note that h is supposed to be the index to the stack top.  
  If it is not, a run-time error happen and REDLIB stops. 

4. Basic runtime environment

The tar file includes the following. 

. This `project-sudoku-guide.txt' file. 
. A make file `sdkmake' for your code compilation.  
  Just type in "make -f sdkmake" and the compilation will be carried out.
. A header file `redlib.h' to be included in your application program in 
  order to use REDLIB.
. A header file `redlib.e' to be included in your application program in 
  order to use REDLIB.  
. An object file `redlib.a' to be compiled with your application program code
  to make a full application out of REDLIB. 
. The source code of sudoku.c for the solving of sudoku game with REDLIB. 
. An executable `sdk' obtained from the compilation of sudoku.c and redlib.a. 
  You can run the file to solve the sudoku game. 
. Three input sample files, 9, 99, and 9981, to sdk. 
  

5. Hints 

Note that all our MBDD+CRD are shared.  
The two shared MBDD+CRD structures are equivalent iff they have the 
same root addresses.  

The problem is solved with high memory complexity.  
It is expected that you may run out of memory soon and 
your hard disk start thrashing.  
So, if you find that your program runs so slowly, almost being like 
idle, you may want execute the following piece of code.  

  top = red_push(sol); 
  red_garbage_collect(RED_GARBAGE_SILENT);                                                                                                                                                                                                                                                                                 
  red_pop(top); 

RED_garbage_collec() will reclaim all the unprotected BDD+CRD+HRDs.  
REDLIB provides a user stack.  
You can protect your BDD+CRD+HRDs by pushing them into the user stack.  
You can unprotect ones by popping them out of the user stack.  


