1 /**************************************************************************
2 BDD demonstration of the N-Queen chess problem.
3 -----------------------------------------------
4 The BDD variables correspond to a NxN chess board like:
5
6 0 N 2N .. N*N-N
7 1 N+1 2N+1 .. N*N-N+1
8 2 N+2 2N+2 .. N*N-N+2
9 .. .. .. .. ..
10 N-1 2N-1 3N-1 .. N*N-1
11
12 So for example a 4x4 is:
13
14 0 4 8 12
15 1 5 9 13
16 2 6 10 14
17 3 7 11 15
18
19 One solution is then that 2,4,11,13 should be true, meaning a queen
20 should be placed there:
21
22 . X . .
23 . . . X
24 X . . .
25 . . X .
26
27 **************************************************************************/
28 #include <stdlib.h>
29 #include "bdd.h"
30
31 int N; /* Size of the chess board */
32 bdd **X; /* BDD variable array */
33 bdd queen; /* N-queen problem express as a BDD */
34
35
36 /* Build the requirements for all other fields than (i,j) assuming
37 that (i,j) has a queen */
build(int i,int j)38 void build(int i, int j)
39 {
40 bdd a=bddtrue, b=bddtrue, c=bddtrue, d=bddtrue;
41 int k,l;
42
43 /* No one in the same column */
44 for (l=0 ; l<N ; l++)
45 if (l != j)
46 a &= X[i][j] >> !X[i][l];
47
48 /* No one in the same row */
49 for (k=0 ; k<N ; k++)
50 if (k != i)
51 b &= X[i][j] >> !X[k][j];
52
53 /* No one in the same up-right diagonal */
54 for (k=0 ; k<N ; k++)
55 {
56 int ll = k-i+j;
57 if (ll>=0 && ll<N)
58 if (k != i)
59 c &= X[i][j] >> !X[k][ll];
60 }
61
62 /* No one in the same down-right diagonal */
63 for (k=0 ; k<N ; k++)
64 {
65 int ll = i+j-k;
66 if (ll>=0 && ll<N)
67 if (k != i)
68 d &= X[i][j] >> !X[k][ll];
69 }
70
71 queen &= a & b & c & d;
72 }
73
74
main(int ac,char ** av)75 int main(int ac, char **av)
76 {
77 using namespace std ;
78 int n,i,j;
79
80 if (ac != 2)
81 {
82 fprintf(stderr, "USAGE: queen N\n");
83 return 1;
84 }
85
86 N = atoi(av[1]);
87 if (N <= 0)
88 {
89 fprintf(stderr, "USAGE: queen N\n");
90 return 1;
91 }
92
93 /* Initialize with 100000 nodes, 10000 cache entries and NxN variables */
94 bdd_init(N*N*256, 10000);
95 bdd_setvarnum(N*N);
96
97 queen = bddtrue;
98
99 /* Build variable array */
100 X = new bdd*[N];
101 for (n=0 ; n<N ; n++)
102 X[n] = new bdd[N];
103
104 for (i=0 ; i<N ; i++)
105 for (j=0 ; j<N ; j++)
106 X[i][j] = bdd_ithvar(i*N+j);
107
108 /* Place a queen in each row */
109 for (i=0 ; i<N ; i++)
110 {
111 bdd e = bddfalse;
112 for (j=0 ; j<N ; j++)
113 e |= X[i][j];
114 queen &= e;
115 }
116
117 /* Build requirements for each variable(field) */
118 for (i=0 ; i<N ; i++)
119 for (j=0 ; j<N ; j++)
120 {
121 cout << "Adding position " << i << "," << j << "\n" << flush;
122 build(i,j);
123 }
124
125 /* Print the results */
126 cout << "There are " << bdd_satcount(queen) << " solutions\n";
127 cout << "one is:\n";
128 bdd solution = bdd_satone(queen);
129 cout << bddset << solution << endl;
130
131 bdd_done();
132
133 return 0;
134 }
135