Project Hamiltonian Cycle


IMPLEMENTATION OF A HAMILTONIAN CYCLE SOLVER BASED ON REDLIB.   

HISTORY

This project was first introduced in the spring of 2008  for the class 
of FORMAL MODELING AND VERIFICATION at National Taiwan University. 

GOAL 

Study the REDLIB package and learn how to use it 
solve board games. 
Any implementation that does not rely on the symbolic reasoning facilities 
of REDLIB will be unacceptable and declined. 

THE HAMILTONIAN CYCLE GAME ON A BOARD

We have a 6-by-6 matrix.  
We are supposed to start our tour from the upper-left corner, 
visit each slot exactly once, and go back to the upper-left corner. 
In an input configuration of a board, 
each slot may be filled with one of the following values. 
0: No restriction to the movement to the slot. 
   A tourist may come from any of the four sides and leave from 
   any of the other three sides.  
1: A tourist may either 
   o enter from the lower side and leave from the right side; or 
   o enter from the right side and leave from the lower side. 
2: A tourist may either 
   o enter from the left side and leave from the lower side; or 
   o enter from the lower side and leave from the left side. 
3: A tourist may either 
   o enter from the upper side and leave from the right side; or 
   o enter from the right side and leave from the upper side. 
4: A tourist may either 
   o enter from the upper side and leave from the left side; or 
   o enter from the left side and leave from the upper side. 
5: A tourist may either 
   o enter from the left side and leave from the right side; or 
   o enter from the right side and leave from the left side. 
6: A tourist may either 
   o enter from the lower side and leave from the upper side; or 
   o enter from the upper side and leave from the lower side.  

INPUT FORMAT 

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

100040
010000
406000
100402
005000
340004

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 `project2-guide080402.txt' file. 
. A three-page explanation.  
. Two input sample files, `yes' and `no', to your program. 
. A folder for our materials for solving the sudoku game.  
. A preliminary draft for the manual of REDLIB. 
. The object file `redlib.a' for REDLIB. 
. The header files `redlib.h' and `redlib.e' for REDLIB. 
  
5. Hints 

You may study the materials for our previous sudoku project for some clues. 
Note that all our MBDD+CRD diagrams are shared.  
The two shared MBDD+CRD structures are equivalent if 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.  


