From f5a37dff2ba1b976be98d9e1987c1713f2f82fd6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= <201505832@post.au.dk> Date: Tue, 26 Jul 2022 22:36:46 +0200 Subject: [PATCH] Replace node_writer with zdd_builder in Knight's Tour example --- docs/examples/knights_tour.md | 330 ++++++++++++++----------------- example/knights_tour.cpp | 362 +++++++++++++++++----------------- 2 files changed, 334 insertions(+), 358 deletions(-) diff --git a/docs/examples/knights_tour.md b/docs/examples/knights_tour.md index 64ad8c4d4..430e625cb 100644 --- a/docs/examples/knights_tour.md +++ b/docs/examples/knights_tour.md @@ -39,9 +39,9 @@ To get around the entire board, the Knight will need to use N2 time-steps. Our variable ordering will represent every *time-slice* together, where the board of each slice is similar to the [Queens example](queens.md). ```cpp -inline adiar::label_t label_of_position(int N, int i, int j, int t) +inline adiar::label_t int_of_position(int N, int r, int c, int t = 0) { - return (N * N * t) + (N * i) + j; + return (N * N * t) + (N * r) + c; } ``` @@ -57,90 +57,74 @@ squares. ```cpp const int closed_squares [3][2] = { {0,0}, {1,2}, {2,1} }; -bool is_closed_square(int i, int j) +bool is_closed_square(int r, int c) { - return (i == closed_squares[0][0] && j == closed_squares[0][1]) - || (i == closed_squares[1][0] && j == closed_squares[1][1]) - || (i == closed_squares[2][0] && j == closed_squares[2][1]); + return (r == closed_squares[0][0] && c == closed_squares[0][1]) + || (r == closed_squares[1][0] && c == closed_squares[1][1]) + || (r == closed_squares[2][0] && c == closed_squares[2][1]); } ``` -To encode the constraint for time step *t* = 0, *t* = 1, and *t* = -N2-1 we need to add a long "don't care" chain in between. Inside of -this chain can also immediately add the -[hamiltonian constraint](#hamiltonian-constraint) to not visit any of these -squares again. +To encode the closed tours, we may force the Knight to start in the top-left +corner and take one of the two solutions. By multiplying with a constant factor, +we can then take the mirrored path and all possible starting positions into +account. + +So we need to encode that the Knight at time step *t* = 0 is at position (0,0), +at *t* = 1 at (1,2), and at *t* = N2-1 at (2,1). This is easy in +ZDDs, since this is equivalent to skipping variables at these three time steps, +such that only the "desired" positions are present and forced to true. + +All remaining time steps remains one long "don't care" chain in between. Yet, +inside of this chain we can encode the hamiltonian constraint for these three +cells on the board by skipping them within the chain. ```cpp -template -void constraint_dont_care(adiar::node_writer &out_writer, adiar::ptr_t &curr_root, - int N, int max_t, int min_t) +adiar::zdd constraint_closed(int N) { - for (int curr_t = max_t; curr_t >= min_t; curr_t--) { - for (int i = N - 1; i >= 0; i--) { - for (int j = N - 1; j >= 0; j--) { - if (filter_closed_squares && is_closed_square(i,j)) { - continue; - } + adiar::zdd_builder builder; + + // Fix t = max_time to be (1,2) + const int max_time = N*N-1; + + const int stepMax_position = int_of_position(N, + closed_squares[2][0], + closed_squares[2][1], + max_time); + + typename adiar::zdd_ptr root = builder.add_node(stepMax_position, false, true); - adiar::node_t out_node = adiar::create_node(label_of_position(N,i,j,curr_t), - 0, - curr_root, - curr_root); + // All in between is as-is but take the hamiltonian constraint into account. + for (int t = max_time - 1; t > 1; t--) { + for (int r = N-1; r >= 0; r--) { + for (int c = N-1; c >= 0; c--) { + if (is_closed_square(r,c)) { continue; } - out_writer << out_node; - curr_root = out_node.uid; + root = builder.add_node(int_of_position(N,r,c,t), root, root); } } } -} -``` -Finally, the following creates the constraint of where to start, go to, and end. + // Fix t = 1 to be (2,1) + const int step1_position = int_of_position(N, + closed_squares[1][0], + closed_squares[1][1], + 1); + root = builder.add_node(step1_position, false, root); -```cpp -adiar::zdd constraint_closed(uint64_t N) -{ - adiar::node_file out; - - { adiar::node_writer out_writer(out); - - // Set final time step to (2,1) - adiar::node_t n_t_end = adiar::create_node(label_of_position(N, - closed_squares[2][0], - closed_squares[2][1], - N*N-1), - adiar::MAX_ID, - adiar::create_terminal_ptr(false), - adiar::create_terminal_ptr(true)); - out_writer << n_t_end; - - // Create don't care on all intermediate steps - adiar::ptr_t curr_root = n_t_end.uid; - constraint_dont_care(out_writer, curr_root, N, N*N-2, 2); - - // Set t = 1 to (1,2) - adiar::node_t n_t_1 = adiar::create_node(label_of_position(N, - closed_squares[1][0], - closed_squares[1][1], - 1), - adiar::MAX_ID, - adiar::create_terminal_ptr(false), - curr_root); - out_writer << n_t_1; - - // Set t = 0 to (0,0) - adiar::node_t n_t_0 = adiar::create_node(label_of_position(N, - closed_squares[0][0], - closed_squares[0][1], - 0), - adiar::MAX_ID, - adiar::create_terminal_ptr(false), - n_t_1.uid); - out_writer << n_t_0; - } + // Fix t = 0 to be (0,0) + const int step0_position = int_of_position(N, + closed_squares[0][0], + closed_squares[0][1], + 0); + root = builder.add_node(step0_position, false, root); + + // Finalize + adiar::zdd out = builder.build(); + + const size_t nodecount = zdd_nodecount(out); + largest_nodes = std::max(largest_nodes, nodecount); - largest_nodes = std::max(largest_nodes, out.size()); return out; } ``` @@ -159,11 +143,11 @@ code computes whether two coordinates represent a legal move. constexpr int row_moves[8] = { -2, -2, -1, -1, 1, 1, 2, 2 }; constexpr int column_moves[8] = { -1, 1, -2, 2, -2, 2, -1, 1 }; -bool is_move(int i_from, int j_from, int i_to, int j_to) +bool is_legal_move(int /*N*/, int r_from, int c_from, int r_to, int c_to) { for (int idx = 0; idx < 8; idx++) { - if (i_from + row_moves[idx] == i_to && - j_from + column_moves[idx] == j_to) { + if (r_from + row_moves[idx] == r_to && + c_from + column_moves[idx] == c_to) { return true; } } @@ -171,119 +155,111 @@ bool is_move(int i_from, int j_from, int i_to, int j_to) } ``` -We will in the later construction of the transition function "iterate" over -these moves (in the order they are defined in the two `constexpr` arrays). Here, -we will also incorporate the time-dimension directly by not returning the tuple -of coordinates but an `adiar::ptr` with said coordinate and already at the next -time step. +This can be extended to whether any position even is reachable. ```cpp -adiar::ptr_t ptr_to_first(int N, int i_from, int j_from, int t) +bool is_legal_position(int N, int r, int c, int t = 0) { - for (int idx = 0; idx < 8; idx++) { - int i_to = i_from + row_moves[idx]; - int j_to = j_from + column_moves[idx]; + if (r < 0 || N-1 < r) { return false; } + if (c < 0 || N-1 < c) { return false; } + if (t < 0 || N*N-1 < t) { return false; } - if (i_to < 0 || N <= i_to || j_to < 0 || N <= j_to) { continue; } - adiar::label_t from_label = label_of_position(N, i_from, j_from, t); - adiar::label_t to_label = label_of_position(N, i_to, j_to, t+1); - - return adiar::create_node_ptr(to_label, from_label); - } - return adiar::create_terminal_ptr(false); + return true; } -adiar::ptr_t ptr_to_next(int N, int i_from, int j_from, int i_to, int j_to, int t) +bool is_reachable(int /*N*/, int r, int c) { - bool seen_move = false; - for (int idx = 0; idx < 8; idx++) { - int i = i_from + row_moves[idx]; - int j = j_from + column_moves[idx]; - - if (i < 0 || N <= i || j < 0 || N <= j) { continue; } - - if (seen_move) { - adiar::label_t from_label = label_of_position(N, i_from, j_from, t); - adiar::label_t to_label = label_of_position(N, i, j, t+1); - - return adiar::create_node_ptr(to_label, from_label); + if (is_legal_position(N, r + row_moves[idx], c + column_moves[idx])) { + return true; } - seen_move = i == i_to && j == j_to; } - return adiar::create_terminal_ptr(false); + return false; } ``` The transition function only encodes the time step *t* to *t+1*. That is, it needs to allow anything to happen at all other time steps. Hence, it also needs a somewhat similar "don't care" chain as the one for the -[closed constraint](#closed-constraint) above but for some other time limits -*min_t* to some *max_t* (inclusive). +[closed constraint](#closed-constraint). Combining everything above, we can create the transition function as follows. ```cpp adiar::zdd constraint_transition(int N, int t) { - adiar::node_file out; - - { // When calling `out.size()` below, we have to make it read-only. So, we - // have to detach the node_writer before we do. This is automatically done - // on garbage collection, which is why we add an inner scope. - adiar::node_writer out_writer(out); - - adiar::ptr_t curr_root = adiar::create_terminal_ptr(true); - - // "Don't care" for future time steps - constraint_dont_care<>(out_writer, curr_root, N, N*N-1, t+2); - - // Node chains at time-step t+1 where exactly one possible square (i',j') is - // visited for every possible one (i,j) at time step t. - for (int i_t1 = N-1; i_t1 >= 0; i_t1--) { - for (int j_t1 = N-1; j_t1 >= 0; j_t1--) { - adiar::label_t next_pos = label_of_position(N, i_t1, j_t1, t+1); - - // We encode the (i,j) inside of the node id to make linking easy. - for (int i_t = N-1; i_t >= 0; i_t--) { - for (int j_t = N-1; j_t >= 0; j_t--) { - - // Is (i',j') reachable from (i,j)? - if (is_move(i_t, j_t, i_t1, j_t1)) { - adiar::label_t curr_pos = label_of_position(N, i_t, j_t, t); - adiar::ptr_t low = ptr_to_next(N, i_t, j_t, i_t1, j_t1, t); - - adiar::node_t out_node = adiar::create_node(next_pos, - curr_pos, - low, - curr_root); - out_writer << out_node; - } - } - } + adiar::zdd_builder builder; + + const int max_cell = N-1; + + // Time steps t' > t+1: + adiar::zdd_ptr post_chain_root = builder.add_node(true); + + const int max_time = N*N-1; + + for (int time = max_time; time > t+1; time--) { + for (int row = max_cell; row >= 0; row--) { + for (int col = max_cell; col >= 0; col--) { + if (!is_reachable(N, row, col)) { continue; } + + const int this_label = int_of_position(N, row, col, time); + post_chain_root = builder.add_node(this_label, + post_chain_root, + post_chain_root); } } + } - // Node chain at time step t - curr_root = adiar::create_terminal_ptr(false); + // Time step t+1: + // Chain with each possible position reachable from some position at time 't'. + std::vector to_chains(N*N, builder.add_node(false)); - for (int i = N-1; i >= 0; i--) { - for (int j = N-1; j >= 0; j--) { - adiar::label_t out_label = label_of_position(N, i, j, t); + for (int row = max_cell; row >= 0; row--) { + for (int col = max_cell; col >= 0; col--) { + const int this_label = int_of_position(N, row, col, t+1); - adiar::ptr_t high = ptr_to_first(N, i, j, t); + for (int row_t = max_cell; row_t >= 0; row_t--) { + for (int col_t = max_cell; col_t >= 0; col_t--) { + if (!is_reachable(N, row_t, col_t)) { continue; } + if (!is_legal_move(N, row_t, col_t, row, col)) { continue; } - adiar::node_t out_node = adiar::create_node(out_label, 0, curr_root, high); + const int vector_idx = int_of_position(N, row_t, col_t); - out_writer << out_node; - curr_root = out_node.uid; + to_chains.at(vector_idx) = builder.add_node(this_label, + to_chains.at(vector_idx), + post_chain_root); + } } } + } + + // Time step t: + // For each position at time step 't', check whether we are "here" and go to + // the chain checking "where we go to" at 't+1'. + typename adiar::zdd_ptr root = builder.add_node(false); + + for (int row = max_cell; row >= 0; row--) { + for (int col = max_cell; col >= 0; col--) { + if (!is_reachable(N, row, col)) { continue; } - // "Don't care" for previous time steps - constraint_dont_care<>(out_writer, curr_root, N, t-1, 0); + const int this_label = int_of_position(N, row, col, t); + const int to_chain_idx = int_of_position(N, row, col); + root = builder.add_node(this_label, root, to_chains.at(to_chain_idx)); + } + } + + // Time-step t' < t: + // Just allow everything, i.e. add no constraints + for (int pos = int_of_position(N, max_cell, max_cell, t-1); pos >= 0; pos--) { + root = builder.add_node(pos, root, root); } + // Finalize + adiar::zdd out = builder.build(); + + const size_t nodecount = zdd_nodecount(out); + largest_nodes = std::max(largest_nodes, nodecount); + return out; } ``` @@ -294,41 +270,39 @@ Only using the above we would obtain *all* paths of length N2; also the ones where a position is visited twice. ```cpp -adiar::zdd constraint_exactly_once(uint64_t N, uint64_t i, uint64_t j) +adiar::zdd constraint_exactly_once(int N, int r, int c) { - adiar::node_file out; + adiar::zdd_builder builder; - { adiar::node_writer out_writer(out); + adiar::zdd_ptr out_never = builder.add_node(false); + adiar::zdd_ptr out_once = builder.add_node(true); - adiar::ptr_t next0 = adiar::create_terminal_ptr(false); - adiar::ptr_t next1 = adiar::create_terminal_ptr(true); + const int max_time = N*N-1; + const int max_cell = N-1; - for (int curr_t = N*N-1; curr_t >= 0; curr_t--) { - for (int curr_i = N-1; curr_i >= 0; curr_i--) { - for (int curr_j = N-1; curr_j >= 0; curr_j--) { - adiar::label_t out_label = label_of_position(N, curr_i, curr_j, curr_t); + for (int this_t = max_time; this_t >= 0; this_t--) { + for (int this_r = max_cell; this_r >= 0; this_r--) { + for (int this_c = max_cell; this_c >= 0; this_c--) { + const int this_label = int_of_position(N, this_r, this_c, this_t); + const bool is_rc = r == this_r && c == this_c; - bool is_ij = i == curr_i && j == curr_j; - - // If we are talking about (i,j) and we already have counted it once, then - // it is forced to zero. In ZDDs this is represented by skipping it. - if (!is_ij && (curr_t > 0 || curr_i > i)) { - adiar::node_t out_n1 = adiar::create_node(out_label, 1, next1, next1); - out_writer << out_n1; - next1 = out_n1.uid; - } - - adiar::node_t out_n0 = adiar::create_node(out_label, 0, - next0, - is_ij ? next1 : next0); - out_writer << out_n0; - next0 = out_n0.uid; + if (!is_rc && (this_t > 0 || this_r > r)) { + out_once = builder.add_node(this_label, out_once, out_once); } + + out_never = builder.add_node(this_label, + out_never, + is_rc ? out_once : out_never); } } } - largest_nodes = std::max(largest_nodes, out.size()); + // Finalize + adiar::zdd out = builder.build(); + + const size_t nodecount = zdd_nodecount(out); + largest_nodes = std::max(largest_nodes, nodecount); + return out; } ``` diff --git a/example/knights_tour.cpp b/example/knights_tour.cpp index 32f7233e0..17d4d1cb0 100644 --- a/example/knights_tour.cpp +++ b/example/knights_tour.cpp @@ -18,16 +18,16 @@ size_t largest_nodes = 1; /******************************************************************************* * Variable ordering * - * (N^2 * t) + (N * i) + j. + * (N^2 * t) + (N * r) + c. * * That is, we encode the entire information about position and time-step into - * the very variable label. This ordering is first by row, second by column, and + * the very variable label. This ordering is first by column, second by row, and * finally by time. Most importantly, this means that any "snapshot" of the * board at a specific time-step are grouped together. */ -inline adiar::label_t label_of_position(int N, int i, int j, int t) +inline adiar::label_t int_of_position(int N, int r, int c, int t = 0) { - return (N * N * t) + (N * i) + j; + return (N * N * t) + (N * r) + c; } /******************************************************************************* @@ -43,93 +43,80 @@ inline adiar::label_t label_of_position(int N, int i, int j, int t) */ const int closed_squares [3][2] = {{0,0}, {1,2}, {2,1}}; -bool is_closed_square(int i, int j) +bool is_closed_square(int r, int c) { - return (i == closed_squares[0][0] && j == closed_squares[0][1]) - || (i == closed_squares[1][0] && j == closed_squares[1][1]) - || (i == closed_squares[2][0] && j == closed_squares[2][1]); + return (r == closed_squares[0][0] && c == closed_squares[0][1]) + || (r == closed_squares[1][0] && c == closed_squares[1][1]) + || (r == closed_squares[2][0] && c == closed_squares[2][1]); } /******************************************************************************* - * Creates a long "don't care" chain for all the positions and times, that we do - * not care about. If we are working with the closed tour, then we can safely - * skip these to make the intermediate ZDDs smaller. + * Combining the above, we can construct the ZDD that fixes the initial + * position, the second position, and the final position while allowing any + * possibilities for anything in between. + * + * * ---- position (0,0) at time 0 + * / \ + * F * ---- position (1,2) at time 1 + * / \ + * F * + * || + * ---- positions at time 2 ... N*N-2 + * || + * * ---- position (2,1) at time N*N-1 + * / \ + * F T */ -template -void constraint_dont_care(adiar::node_writer &out_writer, adiar::ptr_t &curr_root, - int N, int max_t, int min_t) +adiar::zdd constraint_closed(int N) { - for (int curr_t = max_t; curr_t >= min_t; curr_t--) { - for (int i = N - 1; i >= 0; i--) { - for (int j = N - 1; j >= 0; j--) { - if (filter_closed_squares && is_closed_square(i,j)) { - continue; - } + adiar::zdd_builder builder; + + // Fix t = max_time to be (1,2) + const int max_time = N*N-1; + + const int stepMax_position = int_of_position(N, + closed_squares[2][0], + closed_squares[2][1], + max_time); + + typename adiar::zdd_ptr root = builder.add_node(stepMax_position, false, true); - adiar::node_t out_node = adiar::create_node(label_of_position(N,i,j,curr_t), - 0, - curr_root, - curr_root); + // All in between is as-is but take the hamiltonian constraint into account. + for (int t = max_time - 1; t > 1; t--) { + for (int r = N-1; r >= 0; r--) { + for (int c = N-1; c >= 0; c--) { + if (is_closed_square(r,c)) { continue; } - out_writer << out_node; - curr_root = out_node.uid; + root = builder.add_node(int_of_position(N,r,c,t), root, root); } } } -} -/******************************************************************************* - * Combining the above, we can construct the ZDD that fixes the initial - * position, the second position, and the final position. - */ -adiar::zdd constraint_closed(uint64_t N) -{ - adiar::node_file out; - - { adiar::node_writer out_writer(out); - - // Set final time step to (2,1) - adiar::node_t n_t_end = adiar::create_node(label_of_position(N, - closed_squares[2][0], - closed_squares[2][1], - N*N-1), - adiar::MAX_ID, - adiar::create_sink_ptr(false), - adiar::create_sink_ptr(true)); - out_writer << n_t_end; - - // Create don't care on all intermediate steps - adiar::ptr_t curr_root = n_t_end.uid; - constraint_dont_care(out_writer, curr_root, N, N*N-2, 2); - - // Set t = 1 to (1,2) - adiar::node_t n_t_1 = adiar::create_node(label_of_position(N, - closed_squares[1][0], - closed_squares[1][1], - 1), - adiar::MAX_ID, - adiar::create_sink_ptr(false), - curr_root); - out_writer << n_t_1; - - // Set t = 0 to (0,0) - adiar::node_t n_t_0 = adiar::create_node(label_of_position(N, - closed_squares[0][0], - closed_squares[0][1], - 0), - adiar::MAX_ID, - adiar::create_sink_ptr(false), - n_t_1.uid); - out_writer << n_t_0; - } + // Fix t = 1 to be (2,1) + const int step1_position = int_of_position(N, + closed_squares[1][0], + closed_squares[1][1], + 1); + root = builder.add_node(step1_position, false, root); + + // Fix t = 0 to be (0,0) + const int step0_position = int_of_position(N, + closed_squares[0][0], + closed_squares[0][1], + 0); + root = builder.add_node(step0_position, false, root); + + // Finalize + adiar::zdd out = builder.build(); + + const size_t nodecount = zdd_nodecount(out); + largest_nodes = std::max(largest_nodes, nodecount); - largest_nodes = std::max(largest_nodes, out.size()); return out; } - /******************************************************************************* - * Move Logic for Transition Function + * Legal Moves * * We need a little bit of logic to compute the different parts of a move. This * is not the bottleneck, so we will do something somewhat easily comprehensible @@ -141,120 +128,137 @@ adiar::zdd constraint_closed(uint64_t N) constexpr int row_moves[8] = { -2, -2, -1, -1, 1, 1, 2, 2 }; constexpr int column_moves[8] = { -1, 1, -2, 2, -2, 2, -1, 1 }; -bool is_move(int i_from, int j_from, int i_to, int j_to) +bool is_legal_move(int /*N*/, int r_from, int c_from, int r_to, int c_to) { for (int idx = 0; idx < 8; idx++) { - if (i_from + row_moves[idx] == i_to && - j_from + column_moves[idx] == j_to) { + if (r_from + row_moves[idx] == r_to && + c_from + column_moves[idx] == c_to) { return true; } } return false; } -adiar::ptr_t ptr_to_first(int N, int i_from, int j_from, int t) +bool is_legal_position(int N, int r, int c, int t = 0) { - for (int idx = 0; idx < 8; idx++) { - int i_to = i_from + row_moves[idx]; - int j_to = j_from + column_moves[idx]; - - if (i_to < 0 || N <= i_to || j_to < 0 || N <= j_to) { continue; } - adiar::label_t from_label = label_of_position(N, i_from, j_from, t); - adiar::label_t to_label = label_of_position(N, i_to, j_to, t+1); + if (r < 0 || N-1 < r) { return false; } + if (c < 0 || N-1 < c) { return false; } + if (t < 0 || N*N-1 < t) { return false; } - return adiar::create_node_ptr(to_label, from_label); - } - return adiar::create_sink_ptr(false); + return true; } -/* When we have the latest 'legal' move we then also want to obtain the next - 'legal' move, or 'false' if there is none. - */ -adiar::ptr_t ptr_to_next(int N, int i_from, int j_from, int i_to, int j_to, int t) +bool is_reachable(int /*N*/, int r, int c) { - bool seen_move = false; - for (int idx = 0; idx < 8; idx++) { - int i = i_from + row_moves[idx]; - int j = j_from + column_moves[idx]; - - if (i < 0 || N <= i || j < 0 || N <= j) { continue; } - - if (seen_move) { - adiar::label_t from_label = label_of_position(N, i_from, j_from, t); - adiar::label_t to_label = label_of_position(N, i, j, t+1); - - return adiar::create_node_ptr(to_label, from_label); + if (is_legal_position(N, r + row_moves[idx], c + column_moves[idx])) { + return true; } - seen_move = i == i_to && j == j_to; } - return adiar::create_sink_ptr(false); + return false; } /******************************************************************************* - * Transition System + * With the above, we can encode what the legal transitions from one state of + * one time step to the next. To this end, we have a "don't care" chain for time + * steps prior and past the two time steps of interest. At time step t we may + * ask exactly where the Knight is placed to then check whether it is placed in + * any legal position at the next time step. + * + * * + * || + * ---- positions at time t-1 and earlier + * || + * * ---- pos (0,0) at time t + * / \ + * * \ ---- pos (1,0) at time t + * / \ \ + * . . | + * . . | + * . . | + * * ---- pos (1,2) at time t+1 + * / \ + * * \ ---- pos (2,1) at time t+1 + * / \ | + * F \ / + * * + * || + * ---- positions at time t+2 and later + * || + * T */ adiar::zdd constraint_transition(int N, int t) { - adiar::node_file out; - - { // When calling `out.size()` below, we have to make it read-only. So, we - // have to detach the node_writer before we do. This is automatically done - // on garbage collection, which is why we add an inner scope. - adiar::node_writer out_writer(out); - - adiar::ptr_t curr_root = adiar::create_sink_ptr(true); - - // "Don't care" for future time steps - constraint_dont_care<>(out_writer, curr_root, N, N*N-1, t+2); - - // Node chains at time-step t+1 where exactly one possible square (i',j') is - // visited for every possible one (i,j) at time step t. - for (int i_t1 = N-1; i_t1 >= 0; i_t1--) { - for (int j_t1 = N-1; j_t1 >= 0; j_t1--) { - adiar::label_t next_pos = label_of_position(N, i_t1, j_t1, t+1); - - // We encode the (i,j) inside of the node id to make linking easy. - for (int i_t = N-1; i_t >= 0; i_t--) { - for (int j_t = N-1; j_t >= 0; j_t--) { - - // Is (i',j') reachable from (i,j)? - if (is_move(i_t, j_t, i_t1, j_t1)) { - adiar::label_t curr_pos = label_of_position(N, i_t, j_t, t); - adiar::ptr_t low = ptr_to_next(N, i_t, j_t, i_t1, j_t1, t); - - adiar::node_t out_node = adiar::create_node(next_pos, - curr_pos, - low, - curr_root); - out_writer << out_node; - } - } - } + adiar::zdd_builder builder; + + const int max_cell = N-1; + + // Time steps t' > t+1: + adiar::zdd_ptr post_chain_root = builder.add_node(true); + + const int max_time = N*N-1; + + for (int time = max_time; time > t+1; time--) { + for (int row = max_cell; row >= 0; row--) { + for (int col = max_cell; col >= 0; col--) { + if (!is_reachable(N, row, col)) { continue; } + + const int this_label = int_of_position(N, row, col, time); + post_chain_root = builder.add_node(this_label, post_chain_root, post_chain_root); } } + } - // Node chain at time step t - curr_root = adiar::create_sink_ptr(false); + // Time step t+1: + // Chain with each possible position reachable from some position at time 't'. + std::vector to_chains(N*N, builder.add_node(false)); - for (int i = N-1; i >= 0; i--) { - for (int j = N-1; j >= 0; j--) { - adiar::label_t out_label = label_of_position(N, i, j, t); + for (int row = max_cell; row >= 0; row--) { + for (int col = max_cell; col >= 0; col--) { + const int this_label = int_of_position(N, row, col, t+1); - adiar::ptr_t high = ptr_to_first(N, i, j, t); + for (int row_t = max_cell; row_t >= 0; row_t--) { + for (int col_t = max_cell; col_t >= 0; col_t--) { + if (!is_reachable(N, row_t, col_t)) { continue; } + if (!is_legal_move(N, row_t, col_t, row, col)) { continue; } - adiar::node_t out_node = adiar::create_node(out_label, 0, curr_root, high); + const int vector_idx = int_of_position(N, row_t, col_t); - out_writer << out_node; - curr_root = out_node.uid; + to_chains.at(vector_idx) = builder.add_node(this_label, + to_chains.at(vector_idx), + post_chain_root); + } } } + } + + // Time step t: + // For each position at time step 't', check whether we are "here" and go to + // the chain checking "where we go to" at 't+1'. + typename adiar::zdd_ptr root = builder.add_node(false); + + for (int row = max_cell; row >= 0; row--) { + for (int col = max_cell; col >= 0; col--) { + if (!is_reachable(N, row, col)) { continue; } + + const int this_label = int_of_position(N, row, col, t); + const int to_chain_idx = int_of_position(N, row, col); + root = builder.add_node(this_label, root, to_chains.at(to_chain_idx)); + } + } - // "Don't care" for previous time steps - constraint_dont_care<>(out_writer, curr_root, N, t-1, 0); + // Time-step t' < t: + // Just allow everything, i.e. add no constraints + for (int pos = int_of_position(N, max_cell, max_cell, t-1); pos >= 0; pos--) { + root = builder.add_node(pos, root, root); } - largest_nodes = std::max(largest_nodes, out.size()); + // Finalize + adiar::zdd out = builder.build(); + + const size_t nodecount = zdd_nodecount(out); + largest_nodes = std::max(largest_nodes, nodecount); + return out; } @@ -269,41 +273,39 @@ adiar::zdd constraint_transition(int N, int t) * the position is 'seen' as taken then one goes to a second chain of nodes, * where it may not be seen again. */ -adiar::zdd constraint_exactly_once(uint64_t N, uint64_t i, uint64_t j) +adiar::zdd constraint_exactly_once(int N, int r, int c) { - adiar::node_file out; - - { adiar::node_writer out_writer(out); - - adiar::ptr_t next0 = adiar::create_sink_ptr(false); - adiar::ptr_t next1 = adiar::create_sink_ptr(true); + adiar::zdd_builder builder; - for (int curr_t = N*N-1; curr_t >= 0; curr_t--) { - for (int curr_i = N-1; curr_i >= 0; curr_i--) { - for (int curr_j = N-1; curr_j >= 0; curr_j--) { - adiar::label_t out_label = label_of_position(N, curr_i, curr_j, curr_t); + adiar::zdd_ptr out_never = builder.add_node(false); + adiar::zdd_ptr out_once = builder.add_node(true); - bool is_ij = i == curr_i && j == curr_j; + const int max_time = N*N-1; + const int max_cell = N-1; - // If we are talking about (i,j) and we already have counted it once, then - // it is forced to zero. In ZDDs this is represented by skipping it. - if (!is_ij && (curr_t > 0 || curr_i > i)) { - adiar::node_t out_n1 = adiar::create_node(out_label, 1, next1, next1); - out_writer << out_n1; - next1 = out_n1.uid; - } + for (int this_t = max_time; this_t >= 0; this_t--) { + for (int this_r = max_cell; this_r >= 0; this_r--) { + for (int this_c = max_cell; this_c >= 0; this_c--) { + const int this_label = int_of_position(N, this_r, this_c, this_t); + const bool is_rc = r == this_r && c == this_c; - adiar::node_t out_n0 = adiar::create_node(out_label, 0, - next0, - is_ij ? next1 : next0); - out_writer << out_n0; - next0 = out_n0.uid; + if (!is_rc && (this_t > 0 || this_r > r)) { + out_once = builder.add_node(this_label, out_once, out_once); } + + out_never = builder.add_node(this_label, + out_never, + is_rc ? out_once : out_never); } } } - largest_nodes = std::max(largest_nodes, out.size()); + // Finalize + adiar::zdd out = builder.build(); + + const size_t nodecount = zdd_nodecount(out); + largest_nodes = std::max(largest_nodes, nodecount); + return out; } @@ -347,7 +349,7 @@ int main(int argc, char* argv[]) switch(c) { case 'c': // HACK: 'constraint_closed' only works for 3x3 boards and bigger. - only_closed = 3u <= N; + only_closed = 3 <= N; continue; case 'h':