Showing false values sets as true in diagram about dd

[johnyf]

The BDD is represented with complemented edges. Considering a node labeled by a variable x, the outgoing solid edge corresponds to the case x = TRUE, and a dashed outgoing edge to the case x = FALSE. A dashed edge annotated with -1 is a complemented edge, in the sense that it references the negation of the node it points to. For example, a dashed edge pointing to the node labeled with "True" references TRUE, whereas a dashed edge annotated with -1 that points to "True" references FALSE. A more detailed description can be found in Sec. 2.3 of "Binary decision diagrams" by Fabio Somenzi, and in the documentation of plotting.

The variables for the row with index 0 and the column with index 0 appear to be missing from the image. For example, the variables declared include x00 for all problem instances (range):

https://github.com/johnyf/dd/blob/954c7045ae4a62a50ebc2d5ee063e703cc5307a5/examples/queens.py#L24-L26

https://github.com/johnyf/dd/blob/954c7045ae4a62a50ebc2d5ee063e703cc5307a5/examples/queens.py#L112-L114

These variables are included in the formulas:

https://github.com/johnyf/dd/blob/954c7045ae4a62a50ebc2d5ee063e703cc5307a5/examples/queens.py#L48-L49

For the case of n = 3, the BDD manager I obtain is:

The problem is solved for an n-by-n chessboard, where n the argument of the function solve_queens:

https://github.com/johnyf/dd/blob/954c7045ae4a62a50ebc2d5ee063e703cc5307a5/examples/queens.py#L19-L20

Running the script queens.py solves the problem for the range of sizes `0..n_max:

https://github.com/johnyf/dd/blob/954c7045ae4a62a50ebc2d5ee063e703cc5307a5/examples/queens.py#L139

Adding the statements:

print(bdd.count(u))
print(list(bdd.pick_iter(u)))

after the line:

https://github.com/johnyf/dd/blob/954c7045ae4a62a50ebc2d5ee063e703cc5307a5/examples/queens.py#L120

shows the number of solutions, and the solutions as assignments to the variables xij. The results I obtain are:

• n = 0: satisfiable (no variables declared, "zero" size chessboard)
• n = 1: satisfiable, with a single solution (one queen on a chessboard with one square)
• n = 2: unsatisfiable (two queens cannot be placed on a 2-by-2 chessboard without interference)
• n = 3: unsatisfiable (three queens cannot be placed on a 3-by-3 chessboard without interference)
• n = 4: satisfiable, with two solutions, which are symmetric with respect to the symmetries of the chessboard (rotation around the horizontal and vertical axes at the middle of the chessboard, and the diagonals of the chessboard).

The cases of n = 2 and n = 3 can be confirmed by drawing a 2-by-2 and a 3-by-3 chessboard and trying to place on them 2 and 3 queens, respectively.

The solutions for n = 4 can be read in the output of print(list(bdd.pick_iter(u))) (from above), namely:

[{'x01': False, 'x31': True, 'x23': True, 'x20': False,
  'x12': False, 'x11': False, 'x13': False, 'x32': False,
  'x22': False, 'x30': False, 'x21': False, 'x02': True,
  'x33': False, 'x00': False, 'x10': True, 'x03': False},

 {'x01': True, 'x31': False, 'x23': False, 'x20': True,
  'x12': False, 'x11': False, 'x13': True, 'x32': True,
  'x22': False, 'x30': False, 'x21': False, 'x02': False,
  'x33': False, 'x00': False, 'x10': False, 'x03': False}]

For example, the assignment 'x31': True means that a queen is present in the square at row 3 and column 1. The assignment 'x01': False means that there is no queen in the square at row 0 and column 1.

The reference for the N-queens problem mentioned in the docstring of the script queens.py is Sec. 6.1 of "An introduction to binary decision diagrams" by Henrik Andersen.