(*bt*)

(* Backtracking, here are two implementations of the backtracking
   algorithm, bt0 and bt1, applied to the n-queens problem. In the
   n-queens problem one is given an n by n chess board and n queens. The
   n queens are to be placed on the board such that there are no
   "attacks" (that is no queen can take any other). This is an
   instance of the constraint satisfaction problem (csp). A row of
   the board can be considered as a variable, the columns of a row
   as the domain of that variable, and the n-queens constraint as
   a constraint that operates between each pair of variables. *)

fun neq x y = not(x=y);
(* Deliver true if x does not equal y *)

fun abs (x:int) = if x < 0 then ~x else x;

fun nq (r1:int,c1:int) (r2:int,c2:int) = (neq c1 c2) andalso
                                         (neq (abs(r1-r2)) 
                                              (abs(c1-c2)));
(* The n-queens constraint. A board position is represented as a pair,
   (row,column). The nq constraint takes as arguments two positions,
   (r1,c1) and (r2,c2), and delivers true if they are not on the same
   column and are not on the same diagonal. By construction, two 
   positions cannot be on the same row. *)

nq (1,1) (2,4);
 
fun check bp (rk,ck) [] = true
   |check bp (rk,ck) ((rp,cp)::p) = bp (rk,ck) (rp,cp) andalso 
                                    check bp (rk,ck) p;
(* Given a binary predicate bp (generally we will have bp=nq), 
   the kth board position, and the set of past variables (see below, 
   that is p is a list of pairs, where each pair is a board position
   already occupied by a queen) deliver true if bp holds
   between (rk,ck) and all other pairs in p *)

check nq (3,2) [(2,3),(1,1)];

fun bt0 k m n p =
    if k>n orelse (m>n andalso p=[])           (*1*)
    then p                                     (*2*)
    else if m>n                                (*3*)
         then let val (pk,pm)=hd p             (*4*)
              in bt0 pk (pm+1) n (tl p) end    (*5*)
         else if check nq (k,m) p              (*6*)
              then bt0 (k+1) 1 n ((k,m)::p)    (*7*)
              else bt0 k (m+1) n p;            (*8*)
(* Function bt0 (and bt1 below) delivers the first solution to the
   n-queens problem. The arguments are as follows:
   k: is the kth variable (row of the board). This is sometimes
      referred to as the "current" variable.
   m: is the value to be assigned to the kth variable.
   n: is the number of variables.
   p: is the "past" variables, that is the set of instantiations that
      have already been made. Sometimes p is referred to as the set 
      of "labelled" variables. Also the set of "unlabelled" variables
      (not explicitly represented here) may be called the "future"
      variables. Therefore we may have past,current and future.

   An initial call is made as follows: bt 1 1 8  []
   This delivers the first solution to the 8-queens problem.

   (1) If k>n then all variables have been instantiated
       and p is delivered as a result. If m>n and p=[] then
       all values have been tried (unsuccessfully) for the current variable 
       k and there are no past variables to undo, therefore there is
       no solution.
   (3) k<=n and m>n means that all values have been tried,
       unsuccessfully, for the current variable k. Therefore we need
       to undo the instantiation of variable k-1, and attempt the next
       instantiation of k-1 (see 4 and 5 below).
   (4) The instantiation of k-1 is the head of p (hd p). pk is the 
       previously instantiated variable (that is k-1) and pm is the value 
       assigned (the column) of variable pk (that is k-1)
   (5) An attempt is made to instantiate variable pk (that is k-1)
       with its next value (that is pm+1). The set of past variables
       is now the "rest" of p (that is (tl p)). Essentially we
       "chronologically backtrack" from k to k-1.
   (6) k<=n and m<=n. An attempt is made to instantiate the kth 
       variable with the value m. The call "check nq (k,m) p"
       determines if the position (k,m) is consistent with respect to
       the past instantiations in p.
   (7) (k,m) is consistent wrt (with respect to) the past variables.
       The instantiation (k,m) is added to the set of past variables
       and the next variable, k+1, becomes the current variable. 
       An attempt will now be made to instantiate k+1 with the 
       first value from its domain. That is: bt0 (k+1) 1 n ((k,m)::p).
   (8) The instantiation (k,m), of the current variable k, was 
       inconsistent wrt the past variables. Therefore an attempt
       is made to instantiate the current variable k with the
       next value in its domain (namely m+1) *)

val nq8 = bt0 1 1 8 [];

fun fm (k,m,n,p) =            
    if check nq (k,m) p
    then (k+1,1,n,(k,m)::p)
    else (k,m+1,n,p);
(* An alternative way. The 4-tuple (k,m,n,p) represents respectively:
   the current variable k, the value that may be assigned m, the
   number of variables n, and the set of past variables p. 
   Function fm makes a "forward move" through the search space. 
   It delivers the next 4-tuple to be tried.
   If the instantiation (k,m) is consistent with the past variables 
   then deliver (k+1,1,n,(k,m)::p) otherwise deliver (k,m+1,n,p). *)

fm (2,3,4,[(1,1)]);

fun bm (k,m,n,p) =
    let val (kprev,mprev) = (hd p)
    in (kprev,mprev+1,n,tl p) end;
(* Make a "backwards move". Undo the most recent instantiation in p,
   namely kprev, and the next value that may be assigned to kprev. 
   That is (kprev,mprev+1,n,tl p) *)

bm (3,5,4,[(2,3),(1,1)]);

fun bt1 (k,m,n,p) =                    (*0*)
    if k>n orelse (m>n andalso p=[])   (*1*)
    then p                             (*2*)
    else if m>n                        (*3*)
         then bt1(bm(k,m,n,p))         (*4*)
         else bt1(fm(k,m,n,p));        (*5*)
(* The alternative implementation of the backtracking algorithm.
   Note that functions fm and bm take as an argument 4-tuples
   and deliver as result a 4-tuples. Also bt1 takes as argument
   a 4-tuple. Therefore the arguments and results can be passed 
   back and forth freely. This is similar to the approach used
   in the implementation of the cartesian product function and
   the perm function.

  (1) k>n implies a solution exists in p. m>n and p=[] 
      implies that there is no consistent instantiation of variable
      k and there is no past variable to backtrack to, therefore
      there is no solution. p is delivered as a result in (2).
  (3) m>n, all values have been tried, without success, for variable 
      k, therefore continue search after a backward move (4)
  (5) m<=n, attempt an instantiation of k with the value m. That
      is continue the search after making a forward move from k. *)

(* Note that we can say that the 4-tuple (k,m,n,p) is akin to 
   a state vector s, that is decoded via pattern matching by bt1,
   fm and bm. Therefore we should be able to make calls 
   bt1 s, fm s, and bm s. Try it *)

val s = (1,1,8,[]);

val s = fm s;
val s = fm s;
val s = fm s;
val s = fm s;
val s = bm s;
val s = bm s;

val s = (1,1,10,[]);
bt1 s;
bt1 (1,1,10,[]);      (* same as previous call *)
bt1 (1,1,3,[]);       (* no solution when n=3 *)
bt0 1 1 3 [];

(* So what!? 

   (1) Which do you prefer, bt0 or bt1. Let me know.
   (2) Modify bt1 and bt0 such that they deliver all solutions
   (3) Implement a new constraint, the "confused" n-queens constraint
       In "confused" n-queens, n queens have to be placed on an
       n by n board such that: (a) each queen is on its own row
       and (b) each queen attacks all other queens. Get bt0 and bt1
       to deliver all solutions to the "confused" n-queens.
   (4) Allow the constraint to be passed as an argument to bt0 and bt1.
   (5) Modify the existing functions such that a count is maintained
       of the number of consistency checks performed, that is how
       often the binary predicate nq (or cnq for "confused") is called.
   (6) Can you think of a better algorithm than bt. That is can you
       implement a function that will find all solutions and perform
       less consistency checks than bt0/1? This is one of the
       "hottest" research topics in Artificial Intelligence. Can you
       see why? *)