View Javadoc

1   import net.sf.javabdd.*;
2   
3   /***
4    * @author John Whaley
5    */
6   public class NQueens {
7       static BDDFactory B;
8   
9       static boolean TRACE;
10      static int N; /* Size of the chess board */
11      static BDD[][] X; /* BDD variable array */
12      static BDD queen; /* N-queen problem expressed as a BDD */
13      static BDD solution; /* One solution */
14  
15      public static void main(String[] args) {
16          if (args.length != 1) {
17              System.err.println("USAGE:  java NQueens N");
18              return;
19          }
20          N = Integer.parseInt(args[0]);
21          if (N <= 0) {
22              System.err.println("USAGE:  java NQueens N");
23              return;
24          }
25          
26          TRACE = true;
27          long time = System.currentTimeMillis();
28          runTest();
29          freeAll();
30          time = System.currentTimeMillis() - time;
31          System.out.println("Time: "+time/1000.+" seconds");
32          BDDFactory.CacheStats cachestats = B.getCacheStats();
33          if (cachestats != null && cachestats.uniqueAccess > 0) {
34              System.out.println(cachestats);
35          }
36          B.done();
37          B = null;
38      }
39  
40      public static double runTest() {
41  
42          if (B == null) {
43              /* Initialize with reasonable nodes and cache size and NxN variables */
44              String numOfNodes = System.getProperty("bddnodes");
45              int numberOfNodes;
46              if (numOfNodes == null)
47                  numberOfNodes = (int) (Math.pow(4.42, N-6))*1000;
48              else
49                  numberOfNodes = Integer.parseInt(numOfNodes);
50              String cache = System.getProperty("bddcache");
51              int cacheSize;
52              if (cache == null)
53                  cacheSize = 1000;
54              else
55                  cacheSize = Integer.parseInt(cache);
56              numberOfNodes = Math.max(1000, numberOfNodes);
57              B = BDDFactory.init(numberOfNodes, cacheSize);
58          }
59          if (B.varNum() < N * N) B.setVarNum(N * N);
60  
61          queen = B.universe();
62  
63          int i, j;
64  
65          /* Build variable array */
66          X = new BDD[N][N];
67          for (i = 0; i < N; i++)
68              for (j = 0; j < N; j++)
69                  X[i][j] = B.ithVar(i * N + j);
70  
71          /* Place a queen in each row */
72          for (i = 0; i < N; i++) {
73              BDD e = B.zero();
74              for (j = 0; j < N; j++) {
75                  e.orWith(X[i][j].id());
76              }
77              queen.andWith(e);
78          }
79  
80          /* Build requirements for each variable(field) */
81          for (i = 0; i < N; i++)
82              for (j = 0; j < N; j++) {
83                  if (TRACE) System.out.print("Adding position " + i + "," + j+"   \r");
84                  build(i, j);
85              }
86  
87          solution = queen.satOne();
88          
89          double result = queen.satCount();
90          /* Print the results */
91          if (TRACE) {
92              System.out.println("There are " + (long) result + " solutions.");
93              double result2 = solution.satCount();
94              System.out.println("Here is "+(long) result2 + " solution:");
95              solution.printSet();
96              System.out.println();
97          }
98  
99          return result;
100     }
101 
102     public static void freeAll() {
103         for (int i = 0; i < N; i++)
104             for (int j = 0; j < N; j++)
105                 X[i][j].free();
106         queen.free();
107         solution.free();
108     }
109     
110     static void build(int i, int j) {
111         BDD a = B.universe(), b = B.universe(), c = B.universe(), d = B.universe();
112         int k, l;
113 
114         /* No one in the same column */
115         for (l = 0; l < N; l++) {
116             if (l != j) {
117                 BDD u = X[i][l].apply(X[i][j], BDDFactory.nand);
118                 a.andWith(u);
119             }
120         }
121 
122         /* No one in the same row */
123         for (k = 0; k < N; k++) {
124             if (k != i) {
125                 BDD u = X[i][j].apply(X[k][j], BDDFactory.nand);
126                 b.andWith(u);
127             }
128         }
129 
130         /* No one in the same up-right diagonal */
131         for (k = 0; k < N; k++) {
132             int ll = k - i + j;
133             if (ll >= 0 && ll < N) {
134                 if (k != i) {
135                     BDD u = X[i][j].apply(X[k][ll], BDDFactory.nand);
136                     c.andWith(u);
137                 }
138             }
139         }
140 
141         /* No one in the same down-right diagonal */
142         for (k = 0; k < N; k++) {
143             int ll = i + j - k;
144             if (ll >= 0 && ll < N) {
145                 if (k != i) {
146                     BDD u = X[i][j].apply(X[k][ll], BDDFactory.nand);
147                     d.andWith(u);
148                 }
149             }
150         }
151         
152         c.andWith(d);
153         b.andWith(c);
154         a.andWith(b);
155         queen.andWith(a);
156     }
157 
158 }