[Constraint Satisfaction Problem] retour sur trace (backtracking) non chronologique (backjumping)

Je comprends très bien ce qu'est un retour sur trace chronologique.

Par exemple, toutes les solutions au problème du tour de cavalier sur un échiquier en backtracking :

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
MODULE KnightTour;
 
   IMPORT StdLog;
 
   VAR
      board : ARRAY 8 OF ARRAY 8 OF INTEGER;
 
   PROCEDURE Bounded (x,y : INTEGER) : BOOLEAN;
   BEGIN
      IF (x < 0) OR (x > 7) THEN RETURN FALSE END;
      IF (y < 0) OR (y > 7) THEN RETURN FALSE END;
      RETURN TRUE
   END Bounded;
 
   PROCEDURE Print;
      VAR x, y : INTEGER;
   BEGIN
      FOR x := 0 TO 7 DO
         FOR y := 0 TO 7 DO
            StdLog.IntForm(board[x,y], StdLog.decimal, 2 , '0', StdLog.hideBase);
            StdLog.Char(' ')
         END;
         StdLog.Ln
      END;
      StdLog.Ln
   END Print;
 
   PROCEDURE Forward_chaining (n, x, y : INTEGER);
   BEGIN
      IF Bounded(x, y) & (board[x,y] = 0) THEN
         board[x,y] := n;
         IF n = 8 * 8 THEN
            Print
         ELSE
            n := n + 1;
            Forward_chaining(n, x + 1, y + 2);
            Forward_chaining(n, x + 2, y + 1);
            Forward_chaining(n, x + 2, y - 1);
            Forward_chaining(n, x + 1, y - 2);
            Forward_chaining(n, x - 1, y - 2);
            Forward_chaining(n, x - 2, y - 1);
            Forward_chaining(n, x - 2, y + 1);
            Forward_chaining(n, x - 1, y + 2);
         END;
         board[x,y] := 0;        
      END
   END Forward_chaining;   
 
   PROCEDURE Solve_all* ;
   BEGIN
      Forward_chaining(1, 0, 0);
   END Solve_all;
 
END KnightTour.

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
let board =
   Array.make_matrix 8 8 0
 
let bounded x y =
   if x < 0 || x > 7 then false
   else if y < 0 || y > 7 then false
   else true
 
let print_board () =
   Array.iter (fun a -> Array.iter
   (fun k -> if k < 10 then print_char '0'; print_int k; print_char ' ') a;
   print_newline ())
   board
 
let rec forward_chaining n x y =
   if bounded x y && board.(x).(y) = 0 then begin
      board.(x).(y) <- n;
      if n = 8 * 8 then
         (print_board (); print_newline ())
      else begin 
         forward_chaining (n + 1) (x + 1) (y + 2);
         forward_chaining (n + 1) (x + 2) (y + 1);
         forward_chaining (n + 1) (x + 2) (y - 1);
         forward_chaining (n + 1) (x + 1) (y - 2);
         forward_chaining (n + 1) (x - 1) (y - 2);
         forward_chaining (n + 1) (x - 2) (y - 1);
         forward_chaining (n + 1) (x - 2) (y + 1);
         forward_chaining (n + 1) (x - 1) (y + 2);
      end;
      board.(x).(y) <- 0;
   end
 
let () = forward_chaining 1 0 0

Autre exemple, toutes les solutions au problème des 8 reines en backtracking :

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
MODULE Queens;
 
   IMPORT StdLog;
 
   TYPE
 
      PtrQueen = POINTER TO Queen;
      Queen =  EXTENSIBLE RECORD
         row, column : INTEGER;
         neighbor : PtrQueen;
      END;
 
      PtrNullQueen = POINTER TO NullQueen;
      NullQueen =  RECORD (Queen)
      END;
 
   PROCEDURE ^ (self : PtrQueen) Test () : BOOLEAN, NEW;
   PROCEDURE ^ (self : PtrQueen) First () : BOOLEAN, NEW, EXTENSIBLE;
   PROCEDURE ^ (self : PtrQueen) Next () : BOOLEAN, NEW, EXTENSIBLE;
   PROCEDURE ^ (self : PtrQueen) Advance () : BOOLEAN, NEW;
 
   PROCEDURE (self : PtrQueen) Check (r, c : INTEGER) : BOOLEAN, NEW, EXTENSIBLE;
      VAR diff : INTEGER;
   BEGIN
      diff := c - self.column;
      RETURN (self.row = r) OR (self.row + diff = r) OR (self.row - diff = r) OR self.neighbor.Check (r, c)
   END Check;
 
   PROCEDURE (self : PtrQueen) Test () : BOOLEAN, NEW;
   BEGIN
      WHILE self.neighbor.Check (self.row, self.column) DO
         IF ~ self.Advance () THEN RETURN FALSE END
      END;
      RETURN TRUE
   END Test;
 
   PROCEDURE (self : PtrQueen) First () : BOOLEAN, NEW, EXTENSIBLE;
      VAR ignore : BOOLEAN;
   BEGIN
      ignore := self.neighbor.First ();
      self.row := 1;
      RETURN self.Test ()
   END First;
 
   PROCEDURE (self : PtrQueen) Next () : BOOLEAN, NEW, EXTENSIBLE;
   BEGIN
      RETURN self.Advance() & self.Test()
   END Next;
 
   PROCEDURE (self : PtrQueen) Advance () : BOOLEAN, NEW;
   BEGIN
      IF self.row = 8 THEN
         IF self.neighbor.Next () THEN self.row := 0 ELSE RETURN FALSE END
      END;
      INC (self.row);
      RETURN TRUE
   END Advance;
 
   PROCEDURE (self : PtrQueen) Print (), NEW, EXTENSIBLE;
   BEGIN
      StdLog.Int(self.row); StdLog.Char(' '); self.neighbor.Print ()
   END Print;
 
   PROCEDURE NewQueen (c : INTEGER; n : PtrQueen) : PtrQueen; 
      VAR q : PtrQueen; 
   BEGIN
      NEW(q); q.column := c; q.neighbor := n;
      RETURN q
   END NewQueen;
 
   PROCEDURE (self : PtrNullQueen) Check (r, c : INTEGER) : BOOLEAN;
      BEGIN RETURN FALSE END Check;
   PROCEDURE (self : PtrNullQueen) First () : BOOLEAN; BEGIN RETURN FALSE END First;
   PROCEDURE (self : PtrNullQueen) Next () : BOOLEAN; BEGIN RETURN FALSE END Next;
   PROCEDURE (self : PtrNullQueen) Print () ; BEGIN StdLog.Ln END Print;
 
   PROCEDURE Solve_all* ;
      VAR last : PtrQueen; null : PtrNullQueen; i : INTEGER;
   BEGIN
      NEW (null); last := null;
      FOR i := 1 TO 8 DO
         last := NewQueen (i, last)
      END;
      IF ~ last.First () THEN StdLog.String("Zero solution."); StdLog.Ln; RETURN END;
      REPEAT
         last.Print()
      UNTIL ~ last.Next ()
   END Solve_all;
 
END NQueens.

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
let null_queen =
   object
      method first = false 
      method next = false 
      method check (x:int) (y:int) = false 
      method print = print_newline ()
   end
 
class queen column (neighbor:queen) =
   object (self)
      val mutable row = 1
      method check r c =
         let diff = c - column in
         (row = r) ||
         (row + diff = r) || (row - diff = r) ||
         neighbor#check r c
      method private test =
         try
            while neighbor#check row column do
               if not self#advance then raise Exit
            done;
            true
         with
         | Exit -> false
      method first =
         ignore(neighbor#first);
         row <- 1;
         self#test
      method next =
         self#advance && self#test
      method private advance =
         if row = 8 then
            (if neighbor#next then (row <- 1; true) else false)
         else (row <- row + 1; true)
      method  print : unit =
         print_int row; print_char ' '; neighbor#print
   end
 
let () =
   let last = (ref null_queen : queen ref) in
   for i = 1 to 8 do
      last := new queen i !last
   done;
   try
      if not !last#first then (print_string "Zero solution." ; raise Exit);
      while true do
         !last#print;
         if not !last#next then raise Exit
      done
   with Exit -> ()

Ce que je comprends plus mal c'est le retour sur trace non chronologique.
Ou plutôt, je comprends bien qu'il est plus avantageux de remonter plus loin dans les choix passés. Ce que je ne comprends pas c'est comment s'y prendre pour détecter ces opportunités de sauts arrières "longs".

Je manque d'une explication claire ou à défaut d'un exemple de code ou de pseudo-code de backjumping sur un problème simple ou bien connu. Et pourquoi pas sur un problème d'échecs comme les deux présentés ci-dessus et pour lesquels je n'arrive pas à trouver une version en backjumping.