Reputation:
I am looking at the applications of BDD to figure out if it's possible to implement the x,y concept there.
Let me explain.
Let's say I have z of something to distribute in an x,y coordinate plane. The constraints are:
I think integer linear programming can sort this out. For example, with a set of equations, I can represent the constraints above and do linear programming to solve for the exact locations.
But what I am asking is if BDD can help with this?
In other words, can Binary Decision Diagram represent x,y coordinates and can I represent the above constraints with Boolean functions (equivalent to the set of equations above) and BDDs be manipulated to sort out the above constraints for exact locations just like linear programming?
I do not have any concrete examples to show but I think representing x,y coordinates equivalent in Binary is a place to start?
Upvotes: 0
Views: 106
Reputation: 11484
Yes, it is possible to encode the given integer-valued problem of placement over a plane using binary decision diagrams, and thus compute answers (as satisfying assignments). For example, using the Python package omega
(which uses the Python package dd
for BDD computations):
from omega.symbolic import fol
fol = _fol.Context()
# Register integer-valued variables, with ranges of representation using BDDs
fol.declare(x1=(0, 11), y1=(0, 11), x2=(0, 11), y2=(0, 11))
# Encode the problem:
#
# Two points on a Euclidean plane are represented by their Cartesian coordinates
# `x1, y1` and `x2, y2`.
# Each point is in the square mesh `x \in 1..10 /\ y \in 1..10`.
#
# Note that the variables are declared with larger domains,
# in order to ensure that this boundary constraint is representable with the
# resulting BDDs.
#
# The distance between the two points should be the square root of 10.
expr = r'''
(x1 >= 1) /\ (x1 <= 10)
/\ (x2 >= 1) /\ (x2 <= 10)
/\ (y1 >= 1) /\ (y1 <= 10)
/\ (y2 >= 1) /\ (y1 <= 10)
/\ (x1 - x2) * (x1 - x2) + (y1 - y2) * (y1 - y2) = 10
'''
# Solve the problem, by adding creating a BDD for it
u = fol.add_expr(expr)
# Enumerate all solutions (i.e., all satisfying assignments)
# These are all the pairs of points within the box mesh x \in 1..10 /\ y \in 1..10
# that have a distance equal to the square root of 10.
assignments = list(fol.pick_iter(u))
print(assignments)
Using BDDs with distance constraints as above can lead to BDDs that are exponential in size in the number of variables. The reason is that representing multiplication can lead to exponentially-sized BDDs, as proved in https://doi.org/10.1109/12.73590 .
If the constraints are not distance between points, but distance along each axis (i.e., an inequality or equality constraint on the absolute value of x1 - x2
or y1 - y2
, or on both), then exponential complexity is avoided.
The above solves the placement problem over a mesh. This is a discrete placement problem. The continuous placement problem cannot be solved with binary decision diagrams, because it requires floating-point arithmetic.
The program above prints:
[{'x1': 4, 'y1': 5, 'x2': 1, 'y2': 4},
{'x1': 4, 'y1': 9, 'x2': 1, 'y2': 8},
{'x1': 4, 'y1': 3, 'x2': 1, 'y2': 4},
{'x1': 4, 'y1': 7, 'x2': 1, 'y2': 8},
{'x1': 4, 'y1': 1, 'x2': 1, 'y2': 2},
{'x1': 4, 'y1': 5, 'x2': 1, 'y2': 6},
{'x1': 4, 'y1': 9, 'x2': 1, 'y2': 10},
{'x1': 4, 'y1': 3, 'x2': 1, 'y2': 2},
{'x1': 4, 'y1': 7, 'x2': 1, 'y2': 6},
{'x1': 4, 'y1': 4, 'x2': 1, 'y2': 5},
{'x1': 4, 'y1': 8, 'x2': 1, 'y2': 9},
{'x1': 4, 'y1': 2, 'x2': 1, 'y2': 1},
{'x1': 4, 'y1': 6, 'x2': 1, 'y2': 5},
{'x1': 4, 'y1': 10, 'x2': 1, 'y2': 9},
{'x1': 4, 'y1': 4, 'x2': 1, 'y2': 3},
{'x1': 4, 'y1': 8, 'x2': 1, 'y2': 7},
{'x1': 4, 'y1': 2, 'x2': 1, 'y2': 3},
{'x1': 4, 'y1': 6, 'x2': 1, 'y2': 7},
{'x1': 4, 'y1': 10, 'x2': 1, 'y2': 11},
{'x1': 4, 'y1': 1, 'x2': 5, 'y2': 4},
{'x1': 4, 'y1': 5, 'x2': 5, 'y2': 8},
{'x1': 4, 'y1': 9, 'x2': 5, 'y2': 12},
{'x1': 4, 'y1': 7, 'x2': 5, 'y2': 4},
{'x1': 4, 'y1': 5, 'x2': 5, 'y2': 2},
{'x1': 4, 'y1': 9, 'x2': 5, 'y2': 6},
{'x1': 4, 'y1': 3, 'x2': 5, 'y2': 6},
{'x1': 4, 'y1': 7, 'x2': 5, 'y2': 10},
{'x1': 4, 'y1': 4, 'x2': 5, 'y2': 1},
{'x1': 4, 'y1': 8, 'x2': 5, 'y2': 5},
{'x1': 4, 'y1': 2, 'x2': 5, 'y2': 5},
{'x1': 4, 'y1': 6, 'x2': 5, 'y2': 9},
{'x1': 4, 'y1': 10, 'x2': 5, 'y2': 13},
{'x1': 4, 'y1': 4, 'x2': 5, 'y2': 7},
{'x1': 4, 'y1': 8, 'x2': 5, 'y2': 11},
{'x1': 4, 'y1': 6, 'x2': 5, 'y2': 3},
{'x1': 4, 'y1': 10, 'x2': 5, 'y2': 7},
{'x1': 2, 'y1': 1, 'x2': 1, 'y2': 4},
{'x1': 2, 'y1': 5, 'x2': 1, 'y2': 8},
{'x1': 2, 'y1': 9, 'x2': 1, 'y2': 12},
{'x1': 2, 'y1': 7, 'x2': 1, 'y2': 4},
{'x1': 2, 'y1': 5, 'x2': 1, 'y2': 2},
{'x1': 2, 'y1': 9, 'x2': 1, 'y2': 6},
{'x1': 2, 'y1': 3, 'x2': 1, 'y2': 6},
{'x1': 2, 'y1': 7, 'x2': 1, 'y2': 10},
{'x1': 2, 'y1': 4, 'x2': 1, 'y2': 1},
{'x1': 2, 'y1': 8, 'x2': 1, 'y2': 5},
{'x1': 2, 'y1': 2, 'x2': 1, 'y2': 5},
{'x1': 2, 'y1': 6, 'x2': 1, 'y2': 9},
{'x1': 2, 'y1': 10, 'x2': 1, 'y2': 13},
{'x1': 2, 'y1': 4, 'x2': 1, 'y2': 7},
{'x1': 2, 'y1': 8, 'x2': 1, 'y2': 11},
{'x1': 2, 'y1': 6, 'x2': 1, 'y2': 3},
{'x1': 2, 'y1': 10, 'x2': 1, 'y2': 7},
{'x1': 2, 'y1': 5, 'x2': 5, 'y2': 4},
{'x1': 2, 'y1': 9, 'x2': 5, 'y2': 8},
{'x1': 2, 'y1': 3, 'x2': 5, 'y2': 4},
{'x1': 2, 'y1': 7, 'x2': 5, 'y2': 8},
{'x1': 2, 'y1': 1, 'x2': 5, 'y2': 2},
{'x1': 2, 'y1': 5, 'x2': 5, 'y2': 6},
{'x1': 2, 'y1': 9, 'x2': 5, 'y2': 10},
{'x1': 2, 'y1': 3, 'x2': 5, 'y2': 2},
{'x1': 2, 'y1': 7, 'x2': 5, 'y2': 6},
{'x1': 2, 'y1': 4, 'x2': 5, 'y2': 5},
{'x1': 2, 'y1': 8, 'x2': 5, 'y2': 9},
{'x1': 2, 'y1': 2, 'x2': 5, 'y2': 1},
{'x1': 2, 'y1': 6, 'x2': 5, 'y2': 5},
{'x1': 2, 'y1': 10, 'x2': 5, 'y2': 9},
{'x1': 2, 'y1': 4, 'x2': 5, 'y2': 3},
{'x1': 2, 'y1': 8, 'x2': 5, 'y2': 7},
{'x1': 2, 'y1': 2, 'x2': 5, 'y2': 3},
{'x1': 2, 'y1': 6, 'x2': 5, 'y2': 7},
{'x1': 2, 'y1': 10, 'x2': 5, 'y2': 11},
{'x1': 6, 'y1': 1, 'x2': 5, 'y2': 4},
{'x1': 6, 'y1': 5, 'x2': 5, 'y2': 8},
{'x1': 6, 'y1': 9, 'x2': 5, 'y2': 12},
{'x1': 6, 'y1': 7, 'x2': 5, 'y2': 4},
{'x1': 6, 'y1': 5, 'x2': 5, 'y2': 2},
{'x1': 6, 'y1': 9, 'x2': 5, 'y2': 6},
{'x1': 6, 'y1': 3, 'x2': 5, 'y2': 6},
{'x1': 6, 'y1': 7, 'x2': 5, 'y2': 10},
{'x1': 6, 'y1': 4, 'x2': 5, 'y2': 1},
{'x1': 6, 'y1': 8, 'x2': 5, 'y2': 5},
{'x1': 6, 'y1': 2, 'x2': 5, 'y2': 5},
{'x1': 6, 'y1': 6, 'x2': 5, 'y2': 9},
{'x1': 6, 'y1': 10, 'x2': 5, 'y2': 13},
{'x1': 6, 'y1': 4, 'x2': 5, 'y2': 7},
{'x1': 6, 'y1': 8, 'x2': 5, 'y2': 11},
{'x1': 6, 'y1': 6, 'x2': 5, 'y2': 3},
{'x1': 6, 'y1': 10, 'x2': 5, 'y2': 7},
{'x1': 4, 'y1': 1, 'x2': 3, 'y2': 4},
{'x1': 4, 'y1': 5, 'x2': 3, 'y2': 8},
{'x1': 4, 'y1': 9, 'x2': 3, 'y2': 12},
{'x1': 4, 'y1': 7, 'x2': 3, 'y2': 4},
{'x1': 4, 'y1': 5, 'x2': 3, 'y2': 2},
{'x1': 4, 'y1': 9, 'x2': 3, 'y2': 6},
{'x1': 4, 'y1': 3, 'x2': 3, 'y2': 6},
{'x1': 4, 'y1': 7, 'x2': 3, 'y2': 10},
{'x1': 4, 'y1': 4, 'x2': 3, 'y2': 1},
{'x1': 4, 'y1': 8, 'x2': 3, 'y2': 5},
{'x1': 4, 'y1': 2, 'x2': 3, 'y2': 5},
{'x1': 4, 'y1': 6, 'x2': 3, 'y2': 9},
{'x1': 4, 'y1': 10, 'x2': 3, 'y2': 13},
{'x1': 4, 'y1': 4, 'x2': 3, 'y2': 7},
{'x1': 4, 'y1': 8, 'x2': 3, 'y2': 11},
{'x1': 4, 'y1': 6, 'x2': 3, 'y2': 3},
{'x1': 4, 'y1': 10, 'x2': 3, 'y2': 7},
{'x1': 4, 'y1': 5, 'x2': 7, 'y2': 4},
{'x1': 4, 'y1': 9, 'x2': 7, 'y2': 8},
{'x1': 4, 'y1': 3, 'x2': 7, 'y2': 4},
{'x1': 4, 'y1': 7, 'x2': 7, 'y2': 8},
{'x1': 4, 'y1': 1, 'x2': 7, 'y2': 2},
{'x1': 4, 'y1': 5, 'x2': 7, 'y2': 6},
{'x1': 4, 'y1': 9, 'x2': 7, 'y2': 10},
{'x1': 4, 'y1': 3, 'x2': 7, 'y2': 2},
{'x1': 4, 'y1': 7, 'x2': 7, 'y2': 6},
{'x1': 4, 'y1': 4, 'x2': 7, 'y2': 5},
{'x1': 4, 'y1': 8, 'x2': 7, 'y2': 9},
{'x1': 4, 'y1': 2, 'x2': 7, 'y2': 1},
{'x1': 4, 'y1': 6, 'x2': 7, 'y2': 5},
{'x1': 4, 'y1': 10, 'x2': 7, 'y2': 9},
{'x1': 4, 'y1': 4, 'x2': 7, 'y2': 3},
{'x1': 4, 'y1': 8, 'x2': 7, 'y2': 7},
{'x1': 4, 'y1': 2, 'x2': 7, 'y2': 3},
{'x1': 4, 'y1': 6, 'x2': 7, 'y2': 7},
{'x1': 4, 'y1': 10, 'x2': 7, 'y2': 11},
{'x1': 2, 'y1': 1, 'x2': 3, 'y2': 4},
{'x1': 2, 'y1': 5, 'x2': 3, 'y2': 8},
{'x1': 2, 'y1': 9, 'x2': 3, 'y2': 12},
{'x1': 2, 'y1': 7, 'x2': 3, 'y2': 4},
{'x1': 2, 'y1': 5, 'x2': 3, 'y2': 2},
{'x1': 2, 'y1': 9, 'x2': 3, 'y2': 6},
{'x1': 2, 'y1': 3, 'x2': 3, 'y2': 6},
{'x1': 2, 'y1': 7, 'x2': 3, 'y2': 10},
{'x1': 2, 'y1': 4, 'x2': 3, 'y2': 1},
{'x1': 2, 'y1': 8, 'x2': 3, 'y2': 5},
{'x1': 2, 'y1': 2, 'x2': 3, 'y2': 5},
{'x1': 2, 'y1': 6, 'x2': 3, 'y2': 9},
{'x1': 2, 'y1': 10, 'x2': 3, 'y2': 13},
{'x1': 2, 'y1': 4, 'x2': 3, 'y2': 7},
{'x1': 2, 'y1': 8, 'x2': 3, 'y2': 11},
{'x1': 2, 'y1': 6, 'x2': 3, 'y2': 3},
{'x1': 2, 'y1': 10, 'x2': 3, 'y2': 7},
{'x1': 6, 'y1': 5, 'x2': 3, 'y2': 4},
{'x1': 6, 'y1': 9, 'x2': 3, 'y2': 8},
{'x1': 6, 'y1': 3, 'x2': 3, 'y2': 4},
{'x1': 6, 'y1': 7, 'x2': 3, 'y2': 8},
{'x1': 6, 'y1': 1, 'x2': 3, 'y2': 2},
{'x1': 6, 'y1': 5, 'x2': 3, 'y2': 6},
{'x1': 6, 'y1': 9, 'x2': 3, 'y2': 10},
{'x1': 6, 'y1': 3, 'x2': 3, 'y2': 2},
{'x1': 6, 'y1': 7, 'x2': 3, 'y2': 6},
{'x1': 6, 'y1': 4, 'x2': 3, 'y2': 5},
{'x1': 6, 'y1': 8, 'x2': 3, 'y2': 9},
{'x1': 6, 'y1': 2, 'x2': 3, 'y2': 1},
{'x1': 6, 'y1': 6, 'x2': 3, 'y2': 5},
{'x1': 6, 'y1': 10, 'x2': 3, 'y2': 9},
{'x1': 6, 'y1': 4, 'x2': 3, 'y2': 3},
{'x1': 6, 'y1': 8, 'x2': 3, 'y2': 7},
{'x1': 6, 'y1': 2, 'x2': 3, 'y2': 3},
{'x1': 6, 'y1': 6, 'x2': 3, 'y2': 7},
{'x1': 6, 'y1': 10, 'x2': 3, 'y2': 11},
{'x1': 6, 'y1': 1, 'x2': 7, 'y2': 4},
{'x1': 6, 'y1': 5, 'x2': 7, 'y2': 8},
{'x1': 6, 'y1': 9, 'x2': 7, 'y2': 12},
{'x1': 6, 'y1': 7, 'x2': 7, 'y2': 4},
{'x1': 6, 'y1': 5, 'x2': 7, 'y2': 2},
{'x1': 6, 'y1': 9, 'x2': 7, 'y2': 6},
{'x1': 6, 'y1': 3, 'x2': 7, 'y2': 6},
{'x1': 6, 'y1': 7, 'x2': 7, 'y2': 10},
{'x1': 6, 'y1': 4, 'x2': 7, 'y2': 1},
{'x1': 6, 'y1': 8, 'x2': 7, 'y2': 5},
{'x1': 6, 'y1': 2, 'x2': 7, 'y2': 5},
{'x1': 6, 'y1': 6, 'x2': 7, 'y2': 9},
{'x1': 6, 'y1': 10, 'x2': 7, 'y2': 13},
{'x1': 6, 'y1': 4, 'x2': 7, 'y2': 7},
{'x1': 6, 'y1': 8, 'x2': 7, 'y2': 11},
{'x1': 6, 'y1': 6, 'x2': 7, 'y2': 3},
{'x1': 6, 'y1': 10, 'x2': 7, 'y2': 7},
{'x1': 8, 'y1': 5, 'x2': 5, 'y2': 4},
{'x1': 8, 'y1': 9, 'x2': 5, 'y2': 8},
{'x1': 8, 'y1': 3, 'x2': 5, 'y2': 4},
{'x1': 8, 'y1': 7, 'x2': 5, 'y2': 8},
{'x1': 8, 'y1': 1, 'x2': 5, 'y2': 2},
{'x1': 8, 'y1': 5, 'x2': 5, 'y2': 6},
{'x1': 8, 'y1': 9, 'x2': 5, 'y2': 10},
{'x1': 8, 'y1': 3, 'x2': 5, 'y2': 2},
{'x1': 8, 'y1': 7, 'x2': 5, 'y2': 6},
{'x1': 8, 'y1': 4, 'x2': 5, 'y2': 5},
{'x1': 8, 'y1': 8, 'x2': 5, 'y2': 9},
{'x1': 8, 'y1': 2, 'x2': 5, 'y2': 1},
{'x1': 8, 'y1': 6, 'x2': 5, 'y2': 5},
{'x1': 8, 'y1': 10, 'x2': 5, 'y2': 9},
{'x1': 8, 'y1': 4, 'x2': 5, 'y2': 3},
{'x1': 8, 'y1': 8, 'x2': 5, 'y2': 7},
{'x1': 8, 'y1': 2, 'x2': 5, 'y2': 3},
{'x1': 8, 'y1': 6, 'x2': 5, 'y2': 7},
{'x1': 8, 'y1': 10, 'x2': 5, 'y2': 11},
{'x1': 8, 'y1': 1, 'x2': 7, 'y2': 4},
{'x1': 8, 'y1': 5, 'x2': 7, 'y2': 8},
{'x1': 8, 'y1': 9, 'x2': 7, 'y2': 12},
{'x1': 8, 'y1': 7, 'x2': 7, 'y2': 4},
{'x1': 8, 'y1': 5, 'x2': 7, 'y2': 2},
{'x1': 8, 'y1': 9, 'x2': 7, 'y2': 6},
{'x1': 8, 'y1': 3, 'x2': 7, 'y2': 6},
{'x1': 8, 'y1': 7, 'x2': 7, 'y2': 10},
{'x1': 8, 'y1': 4, 'x2': 7, 'y2': 1},
{'x1': 8, 'y1': 8, 'x2': 7, 'y2': 5},
{'x1': 8, 'y1': 2, 'x2': 7, 'y2': 5},
{'x1': 8, 'y1': 6, 'x2': 7, 'y2': 9},
{'x1': 8, 'y1': 10, 'x2': 7, 'y2': 13},
{'x1': 8, 'y1': 4, 'x2': 7, 'y2': 7},
{'x1': 8, 'y1': 8, 'x2': 7, 'y2': 11},
{'x1': 8, 'y1': 6, 'x2': 7, 'y2': 3},
{'x1': 8, 'y1': 10, 'x2': 7, 'y2': 7},
{'x1': 10, 'y1': 5, 'x2': 7, 'y2': 4},
{'x1': 10, 'y1': 9, 'x2': 7, 'y2': 8},
{'x1': 10, 'y1': 3, 'x2': 7, 'y2': 4},
{'x1': 10, 'y1': 7, 'x2': 7, 'y2': 8},
{'x1': 10, 'y1': 1, 'x2': 7, 'y2': 2},
{'x1': 10, 'y1': 5, 'x2': 7, 'y2': 6},
{'x1': 10, 'y1': 9, 'x2': 7, 'y2': 10},
{'x1': 10, 'y1': 3, 'x2': 7, 'y2': 2},
{'x1': 10, 'y1': 7, 'x2': 7, 'y2': 6},
{'x1': 10, 'y1': 4, 'x2': 7, 'y2': 5},
{'x1': 10, 'y1': 8, 'x2': 7, 'y2': 9},
{'x1': 10, 'y1': 2, 'x2': 7, 'y2': 1},
{'x1': 10, 'y1': 6, 'x2': 7, 'y2': 5},
{'x1': 10, 'y1': 10, 'x2': 7, 'y2': 9},
{'x1': 10, 'y1': 4, 'x2': 7, 'y2': 3},
{'x1': 10, 'y1': 8, 'x2': 7, 'y2': 7},
{'x1': 10, 'y1': 2, 'x2': 7, 'y2': 3},
{'x1': 10, 'y1': 6, 'x2': 7, 'y2': 7},
{'x1': 10, 'y1': 10, 'x2': 7, 'y2': 11},
{'x1': 6, 'y1': 5, 'x2': 9, 'y2': 4},
{'x1': 6, 'y1': 9, 'x2': 9, 'y2': 8},
{'x1': 6, 'y1': 3, 'x2': 9, 'y2': 4},
{'x1': 6, 'y1': 7, 'x2': 9, 'y2': 8},
{'x1': 6, 'y1': 1, 'x2': 9, 'y2': 2},
{'x1': 6, 'y1': 5, 'x2': 9, 'y2': 6},
{'x1': 6, 'y1': 9, 'x2': 9, 'y2': 10},
{'x1': 6, 'y1': 3, 'x2': 9, 'y2': 2},
{'x1': 6, 'y1': 7, 'x2': 9, 'y2': 6},
{'x1': 6, 'y1': 4, 'x2': 9, 'y2': 5},
{'x1': 6, 'y1': 8, 'x2': 9, 'y2': 9},
{'x1': 6, 'y1': 2, 'x2': 9, 'y2': 1},
{'x1': 6, 'y1': 6, 'x2': 9, 'y2': 5},
{'x1': 6, 'y1': 10, 'x2': 9, 'y2': 9},
{'x1': 6, 'y1': 4, 'x2': 9, 'y2': 3},
{'x1': 6, 'y1': 8, 'x2': 9, 'y2': 7},
{'x1': 6, 'y1': 2, 'x2': 9, 'y2': 3},
{'x1': 6, 'y1': 6, 'x2': 9, 'y2': 7},
{'x1': 6, 'y1': 10, 'x2': 9, 'y2': 11},
{'x1': 8, 'y1': 1, 'x2': 9, 'y2': 4},
{'x1': 10, 'y1': 1, 'x2': 9, 'y2': 4},
{'x1': 8, 'y1': 5, 'x2': 9, 'y2': 8},
{'x1': 10, 'y1': 5, 'x2': 9, 'y2': 8},
{'x1': 8, 'y1': 9, 'x2': 9, 'y2': 12},
{'x1': 10, 'y1': 9, 'x2': 9, 'y2': 12},
{'x1': 8, 'y1': 7, 'x2': 9, 'y2': 4},
{'x1': 10, 'y1': 7, 'x2': 9, 'y2': 4},
{'x1': 8, 'y1': 5, 'x2': 9, 'y2': 2},
{'x1': 10, 'y1': 5, 'x2': 9, 'y2': 2},
{'x1': 8, 'y1': 9, 'x2': 9, 'y2': 6},
{'x1': 10, 'y1': 9, 'x2': 9, 'y2': 6},
{'x1': 8, 'y1': 3, 'x2': 9, 'y2': 6},
{'x1': 10, 'y1': 3, 'x2': 9, 'y2': 6},
{'x1': 8, 'y1': 7, 'x2': 9, 'y2': 10},
{'x1': 10, 'y1': 7, 'x2': 9, 'y2': 10},
{'x1': 8, 'y1': 4, 'x2': 9, 'y2': 1},
{'x1': 10, 'y1': 4, 'x2': 9, 'y2': 1},
{'x1': 8, 'y1': 8, 'x2': 9, 'y2': 5},
{'x1': 10, 'y1': 8, 'x2': 9, 'y2': 5},
{'x1': 8, 'y1': 2, 'x2': 9, 'y2': 5},
{'x1': 10, 'y1': 2, 'x2': 9, 'y2': 5},
{'x1': 8, 'y1': 6, 'x2': 9, 'y2': 9},
{'x1': 10, 'y1': 6, 'x2': 9, 'y2': 9},
{'x1': 8, 'y1': 10, 'x2': 9, 'y2': 13},
{'x1': 10, 'y1': 10, 'x2': 9, 'y2': 13},
{'x1': 8, 'y1': 4, 'x2': 9, 'y2': 7},
{'x1': 10, 'y1': 4, 'x2': 9, 'y2': 7},
{'x1': 8, 'y1': 8, 'x2': 9, 'y2': 11},
{'x1': 10, 'y1': 8, 'x2': 9, 'y2': 11},
{'x1': 8, 'y1': 6, 'x2': 9, 'y2': 3},
{'x1': 10, 'y1': 6, 'x2': 9, 'y2': 3},
{'x1': 8, 'y1': 10, 'x2': 9, 'y2': 7},
{'x1': 10, 'y1': 10, 'x2': 9, 'y2': 7},
{'x1': 1, 'y1': 5, 'x2': 4, 'y2': 4},
{'x1': 1, 'y1': 9, 'x2': 4, 'y2': 8},
{'x1': 1, 'y1': 3, 'x2': 4, 'y2': 4},
{'x1': 1, 'y1': 7, 'x2': 4, 'y2': 8},
{'x1': 1, 'y1': 1, 'x2': 4, 'y2': 2},
{'x1': 1, 'y1': 5, 'x2': 4, 'y2': 6},
{'x1': 1, 'y1': 9, 'x2': 4, 'y2': 10},
{'x1': 1, 'y1': 3, 'x2': 4, 'y2': 2},
{'x1': 1, 'y1': 7, 'x2': 4, 'y2': 6},
{'x1': 1, 'y1': 4, 'x2': 4, 'y2': 5},
{'x1': 1, 'y1': 8, 'x2': 4, 'y2': 9},
{'x1': 1, 'y1': 2, 'x2': 4, 'y2': 1},
{'x1': 1, 'y1': 6, 'x2': 4, 'y2': 5},
{'x1': 1, 'y1': 10, 'x2': 4, 'y2': 9},
{'x1': 1, 'y1': 4, 'x2': 4, 'y2': 3},
{'x1': 1, 'y1': 8, 'x2': 4, 'y2': 7},
{'x1': 1, 'y1': 2, 'x2': 4, 'y2': 3},
{'x1': 1, 'y1': 6, 'x2': 4, 'y2': 7},
{'x1': 1, 'y1': 10, 'x2': 4, 'y2': 11},
{'x1': 5, 'y1': 1, 'x2': 4, 'y2': 4},
{'x1': 5, 'y1': 5, 'x2': 4, 'y2': 8},
{'x1': 5, 'y1': 9, 'x2': 4, 'y2': 12},
{'x1': 5, 'y1': 7, 'x2': 4, 'y2': 4},
{'x1': 5, 'y1': 5, 'x2': 4, 'y2': 2},
{'x1': 5, 'y1': 9, 'x2': 4, 'y2': 6},
{'x1': 5, 'y1': 3, 'x2': 4, 'y2': 6},
{'x1': 5, 'y1': 7, 'x2': 4, 'y2': 10},
{'x1': 5, 'y1': 4, 'x2': 4, 'y2': 1},
{'x1': 5, 'y1': 8, 'x2': 4, 'y2': 5},
{'x1': 5, 'y1': 2, 'x2': 4, 'y2': 5},
{'x1': 5, 'y1': 6, 'x2': 4, 'y2': 9},
{'x1': 5, 'y1': 10, 'x2': 4, 'y2': 13},
{'x1': 5, 'y1': 4, 'x2': 4, 'y2': 7},
{'x1': 5, 'y1': 8, 'x2': 4, 'y2': 11},
{'x1': 5, 'y1': 6, 'x2': 4, 'y2': 3},
{'x1': 5, 'y1': 10, 'x2': 4, 'y2': 7},
{'x1': 3, 'y1': 1, 'x2': 4, 'y2': 4},
{'x1': 3, 'y1': 5, 'x2': 4, 'y2': 8},
{'x1': 3, 'y1': 9, 'x2': 4, 'y2': 12},
{'x1': 3, 'y1': 7, 'x2': 4, 'y2': 4},
{'x1': 3, 'y1': 5, 'x2': 4, 'y2': 2},
{'x1': 3, 'y1': 9, 'x2': 4, 'y2': 6},
{'x1': 3, 'y1': 3, 'x2': 4, 'y2': 6},
{'x1': 3, 'y1': 7, 'x2': 4, 'y2': 10},
{'x1': 3, 'y1': 4, 'x2': 4, 'y2': 1},
{'x1': 3, 'y1': 8, 'x2': 4, 'y2': 5},
{'x1': 3, 'y1': 2, 'x2': 4, 'y2': 5},
{'x1': 3, 'y1': 6, 'x2': 4, 'y2': 9},
{'x1': 3, 'y1': 10, 'x2': 4, 'y2': 13},
{'x1': 3, 'y1': 4, 'x2': 4, 'y2': 7},
{'x1': 3, 'y1': 8, 'x2': 4, 'y2': 11},
{'x1': 3, 'y1': 6, 'x2': 4, 'y2': 3},
{'x1': 3, 'y1': 10, 'x2': 4, 'y2': 7},
{'x1': 7, 'y1': 5, 'x2': 4, 'y2': 4},
{'x1': 7, 'y1': 9, 'x2': 4, 'y2': 8},
{'x1': 7, 'y1': 3, 'x2': 4, 'y2': 4},
{'x1': 7, 'y1': 7, 'x2': 4, 'y2': 8},
{'x1': 7, 'y1': 1, 'x2': 4, 'y2': 2},
{'x1': 7, 'y1': 5, 'x2': 4, 'y2': 6},
{'x1': 7, 'y1': 9, 'x2': 4, 'y2': 10},
{'x1': 7, 'y1': 3, 'x2': 4, 'y2': 2},
{'x1': 7, 'y1': 7, 'x2': 4, 'y2': 6},
{'x1': 7, 'y1': 4, 'x2': 4, 'y2': 5},
{'x1': 7, 'y1': 8, 'x2': 4, 'y2': 9},
{'x1': 7, 'y1': 2, 'x2': 4, 'y2': 1},
{'x1': 7, 'y1': 6, 'x2': 4, 'y2': 5},
{'x1': 7, 'y1': 10, 'x2': 4, 'y2': 9},
{'x1': 7, 'y1': 4, 'x2': 4, 'y2': 3},
{'x1': 7, 'y1': 8, 'x2': 4, 'y2': 7},
{'x1': 7, 'y1': 2, 'x2': 4, 'y2': 3},
{'x1': 7, 'y1': 6, 'x2': 4, 'y2': 7},
{'x1': 7, 'y1': 10, 'x2': 4, 'y2': 11},
{'x1': 1, 'y1': 1, 'x2': 2, 'y2': 4},
{'x1': 1, 'y1': 5, 'x2': 2, 'y2': 8},
{'x1': 1, 'y1': 9, 'x2': 2, 'y2': 12},
{'x1': 1, 'y1': 7, 'x2': 2, 'y2': 4},
{'x1': 1, 'y1': 5, 'x2': 2, 'y2': 2},
{'x1': 1, 'y1': 9, 'x2': 2, 'y2': 6},
{'x1': 1, 'y1': 3, 'x2': 2, 'y2': 6},
{'x1': 1, 'y1': 7, 'x2': 2, 'y2': 10},
{'x1': 1, 'y1': 4, 'x2': 2, 'y2': 1},
{'x1': 1, 'y1': 8, 'x2': 2, 'y2': 5},
{'x1': 1, 'y1': 2, 'x2': 2, 'y2': 5},
{'x1': 1, 'y1': 6, 'x2': 2, 'y2': 9},
{'x1': 1, 'y1': 10, 'x2': 2, 'y2': 13},
{'x1': 1, 'y1': 4, 'x2': 2, 'y2': 7},
{'x1': 1, 'y1': 8, 'x2': 2, 'y2': 11},
{'x1': 1, 'y1': 6, 'x2': 2, 'y2': 3},
{'x1': 1, 'y1': 10, 'x2': 2, 'y2': 7},
{'x1': 5, 'y1': 5, 'x2': 2, 'y2': 4},
{'x1': 5, 'y1': 9, 'x2': 2, 'y2': 8},
{'x1': 5, 'y1': 3, 'x2': 2, 'y2': 4},
{'x1': 5, 'y1': 7, 'x2': 2, 'y2': 8},
{'x1': 5, 'y1': 1, 'x2': 2, 'y2': 2},
{'x1': 5, 'y1': 5, 'x2': 2, 'y2': 6},
{'x1': 5, 'y1': 9, 'x2': 2, 'y2': 10},
{'x1': 5, 'y1': 3, 'x2': 2, 'y2': 2},
{'x1': 5, 'y1': 7, 'x2': 2, 'y2': 6},
{'x1': 5, 'y1': 4, 'x2': 2, 'y2': 5},
{'x1': 5, 'y1': 8, 'x2': 2, 'y2': 9},
{'x1': 5, 'y1': 2, 'x2': 2, 'y2': 1},
{'x1': 5, 'y1': 6, 'x2': 2, 'y2': 5},
{'x1': 5, 'y1': 10, 'x2': 2, 'y2': 9},
{'x1': 5, 'y1': 4, 'x2': 2, 'y2': 3},
{'x1': 5, 'y1': 8, 'x2': 2, 'y2': 7},
{'x1': 5, 'y1': 2, 'x2': 2, 'y2': 3},
{'x1': 5, 'y1': 6, 'x2': 2, 'y2': 7},
{'x1': 5, 'y1': 10, 'x2': 2, 'y2': 11},
{'x1': 5, 'y1': 1, 'x2': 6, 'y2': 4},
{'x1': 5, 'y1': 5, 'x2': 6, 'y2': 8},
{'x1': 5, 'y1': 9, 'x2': 6, 'y2': 12},
{'x1': 5, 'y1': 7, 'x2': 6, 'y2': 4},
{'x1': 5, 'y1': 5, 'x2': 6, 'y2': 2},
{'x1': 5, 'y1': 9, 'x2': 6, 'y2': 6},
{'x1': 5, 'y1': 3, 'x2': 6, 'y2': 6},
{'x1': 5, 'y1': 7, 'x2': 6, 'y2': 10},
{'x1': 5, 'y1': 4, 'x2': 6, 'y2': 1},
{'x1': 5, 'y1': 8, 'x2': 6, 'y2': 5},
{'x1': 5, 'y1': 2, 'x2': 6, 'y2': 5},
{'x1': 5, 'y1': 6, 'x2': 6, 'y2': 9},
{'x1': 5, 'y1': 10, 'x2': 6, 'y2': 13},
{'x1': 5, 'y1': 4, 'x2': 6, 'y2': 7},
{'x1': 5, 'y1': 8, 'x2': 6, 'y2': 11},
{'x1': 5, 'y1': 6, 'x2': 6, 'y2': 3},
{'x1': 5, 'y1': 10, 'x2': 6, 'y2': 7},
{'x1': 3, 'y1': 1, 'x2': 2, 'y2': 4},
{'x1': 3, 'y1': 5, 'x2': 2, 'y2': 8},
{'x1': 3, 'y1': 9, 'x2': 2, 'y2': 12},
{'x1': 3, 'y1': 7, 'x2': 2, 'y2': 4},
{'x1': 3, 'y1': 5, 'x2': 2, 'y2': 2},
{'x1': 3, 'y1': 9, 'x2': 2, 'y2': 6},
{'x1': 3, 'y1': 3, 'x2': 2, 'y2': 6},
{'x1': 3, 'y1': 7, 'x2': 2, 'y2': 10},
{'x1': 3, 'y1': 4, 'x2': 2, 'y2': 1},
{'x1': 3, 'y1': 8, 'x2': 2, 'y2': 5},
{'x1': 3, 'y1': 2, 'x2': 2, 'y2': 5},
{'x1': 3, 'y1': 6, 'x2': 2, 'y2': 9},
{'x1': 3, 'y1': 10, 'x2': 2, 'y2': 13},
{'x1': 3, 'y1': 4, 'x2': 2, 'y2': 7},
{'x1': 3, 'y1': 8, 'x2': 2, 'y2': 11},
{'x1': 3, 'y1': 6, 'x2': 2, 'y2': 3},
{'x1': 3, 'y1': 10, 'x2': 2, 'y2': 7},
{'x1': 3, 'y1': 5, 'x2': 6, 'y2': 4},
{'x1': 3, 'y1': 9, 'x2': 6, 'y2': 8},
{'x1': 3, 'y1': 3, 'x2': 6, 'y2': 4},
{'x1': 3, 'y1': 7, 'x2': 6, 'y2': 8},
{'x1': 3, 'y1': 1, 'x2': 6, 'y2': 2},
{'x1': 3, 'y1': 5, 'x2': 6, 'y2': 6},
{'x1': 3, 'y1': 9, 'x2': 6, 'y2': 10},
{'x1': 3, 'y1': 3, 'x2': 6, 'y2': 2},
{'x1': 3, 'y1': 7, 'x2': 6, 'y2': 6},
{'x1': 3, 'y1': 4, 'x2': 6, 'y2': 5},
{'x1': 3, 'y1': 8, 'x2': 6, 'y2': 9},
{'x1': 3, 'y1': 2, 'x2': 6, 'y2': 1},
{'x1': 3, 'y1': 6, 'x2': 6, 'y2': 5},
{'x1': 3, 'y1': 10, 'x2': 6, 'y2': 9},
{'x1': 3, 'y1': 4, 'x2': 6, 'y2': 3},
{'x1': 3, 'y1': 8, 'x2': 6, 'y2': 7},
{'x1': 3, 'y1': 2, 'x2': 6, 'y2': 3},
{'x1': 3, 'y1': 6, 'x2': 6, 'y2': 7},
{'x1': 3, 'y1': 10, 'x2': 6, 'y2': 11},
{'x1': 7, 'y1': 1, 'x2': 6, 'y2': 4},
{'x1': 7, 'y1': 5, 'x2': 6, 'y2': 8},
{'x1': 7, 'y1': 9, 'x2': 6, 'y2': 12},
{'x1': 7, 'y1': 7, 'x2': 6, 'y2': 4},
{'x1': 7, 'y1': 5, 'x2': 6, 'y2': 2},
{'x1': 7, 'y1': 9, 'x2': 6, 'y2': 6},
{'x1': 7, 'y1': 3, 'x2': 6, 'y2': 6},
{'x1': 7, 'y1': 7, 'x2': 6, 'y2': 10},
{'x1': 7, 'y1': 4, 'x2': 6, 'y2': 1},
{'x1': 7, 'y1': 8, 'x2': 6, 'y2': 5},
{'x1': 7, 'y1': 2, 'x2': 6, 'y2': 5},
{'x1': 7, 'y1': 6, 'x2': 6, 'y2': 9},
{'x1': 7, 'y1': 10, 'x2': 6, 'y2': 13},
{'x1': 7, 'y1': 4, 'x2': 6, 'y2': 7},
{'x1': 7, 'y1': 8, 'x2': 6, 'y2': 11},
{'x1': 7, 'y1': 6, 'x2': 6, 'y2': 3},
{'x1': 7, 'y1': 10, 'x2': 6, 'y2': 7},
{'x1': 9, 'y1': 5, 'x2': 6, 'y2': 4},
{'x1': 9, 'y1': 9, 'x2': 6, 'y2': 8},
{'x1': 9, 'y1': 3, 'x2': 6, 'y2': 4},
{'x1': 9, 'y1': 7, 'x2': 6, 'y2': 8},
{'x1': 9, 'y1': 1, 'x2': 6, 'y2': 2},
{'x1': 9, 'y1': 5, 'x2': 6, 'y2': 6},
{'x1': 9, 'y1': 9, 'x2': 6, 'y2': 10},
{'x1': 9, 'y1': 3, 'x2': 6, 'y2': 2},
{'x1': 9, 'y1': 7, 'x2': 6, 'y2': 6},
{'x1': 9, 'y1': 4, 'x2': 6, 'y2': 5},
{'x1': 9, 'y1': 8, 'x2': 6, 'y2': 9},
{'x1': 9, 'y1': 2, 'x2': 6, 'y2': 1},
{'x1': 9, 'y1': 6, 'x2': 6, 'y2': 5},
{'x1': 9, 'y1': 10, 'x2': 6, 'y2': 9},
{'x1': 9, 'y1': 4, 'x2': 6, 'y2': 3},
{'x1': 9, 'y1': 8, 'x2': 6, 'y2': 7},
{'x1': 9, 'y1': 2, 'x2': 6, 'y2': 3},
{'x1': 9, 'y1': 6, 'x2': 6, 'y2': 7},
{'x1': 9, 'y1': 10, 'x2': 6, 'y2': 11},
{'x1': 5, 'y1': 5, 'x2': 8, 'y2': 4},
{'x1': 5, 'y1': 9, 'x2': 8, 'y2': 8},
{'x1': 5, 'y1': 3, 'x2': 8, 'y2': 4},
{'x1': 5, 'y1': 7, 'x2': 8, 'y2': 8},
{'x1': 5, 'y1': 1, 'x2': 8, 'y2': 2},
{'x1': 5, 'y1': 5, 'x2': 8, 'y2': 6},
{'x1': 5, 'y1': 9, 'x2': 8, 'y2': 10},
{'x1': 5, 'y1': 3, 'x2': 8, 'y2': 2},
{'x1': 5, 'y1': 7, 'x2': 8, 'y2': 6},
{'x1': 5, 'y1': 4, 'x2': 8, 'y2': 5},
{'x1': 5, 'y1': 8, 'x2': 8, 'y2': 9},
{'x1': 5, 'y1': 2, 'x2': 8, 'y2': 1},
{'x1': 5, 'y1': 6, 'x2': 8, 'y2': 5},
{'x1': 5, 'y1': 10, 'x2': 8, 'y2': 9},
{'x1': 5, 'y1': 4, 'x2': 8, 'y2': 3},
{'x1': 5, 'y1': 8, 'x2': 8, 'y2': 7},
{'x1': 5, 'y1': 2, 'x2': 8, 'y2': 3},
{'x1': 5, 'y1': 6, 'x2': 8, 'y2': 7},
{'x1': 5, 'y1': 10, 'x2': 8, 'y2': 11},
{'x1': 7, 'y1': 1, 'x2': 8, 'y2': 4},
{'x1': 7, 'y1': 5, 'x2': 8, 'y2': 8},
{'x1': 7, 'y1': 9, 'x2': 8, 'y2': 12},
{'x1': 7, 'y1': 7, 'x2': 8, 'y2': 4},
{'x1': 7, 'y1': 5, 'x2': 8, 'y2': 2},
{'x1': 7, 'y1': 9, 'x2': 8, 'y2': 6},
{'x1': 7, 'y1': 3, 'x2': 8, 'y2': 6},
{'x1': 7, 'y1': 7, 'x2': 8, 'y2': 10},
{'x1': 7, 'y1': 4, 'x2': 8, 'y2': 1},
{'x1': 7, 'y1': 8, 'x2': 8, 'y2': 5},
{'x1': 7, 'y1': 2, 'x2': 8, 'y2': 5},
{'x1': 7, 'y1': 6, 'x2': 8, 'y2': 9},
{'x1': 7, 'y1': 10, 'x2': 8, 'y2': 13},
{'x1': 7, 'y1': 4, 'x2': 8, 'y2': 7},
{'x1': 7, 'y1': 8, 'x2': 8, 'y2': 11},
{'x1': 7, 'y1': 6, 'x2': 8, 'y2': 3},
{'x1': 7, 'y1': 10, 'x2': 8, 'y2': 7},
{'x1': 7, 'y1': 5, 'x2': 10, 'y2': 4},
{'x1': 7, 'y1': 9, 'x2': 10, 'y2': 8},
{'x1': 7, 'y1': 3, 'x2': 10, 'y2': 4},
{'x1': 7, 'y1': 7, 'x2': 10, 'y2': 8},
{'x1': 7, 'y1': 1, 'x2': 10, 'y2': 2},
{'x1': 7, 'y1': 5, 'x2': 10, 'y2': 6},
{'x1': 7, 'y1': 9, 'x2': 10, 'y2': 10},
{'x1': 7, 'y1': 3, 'x2': 10, 'y2': 2},
{'x1': 7, 'y1': 7, 'x2': 10, 'y2': 6},
{'x1': 7, 'y1': 4, 'x2': 10, 'y2': 5},
{'x1': 7, 'y1': 8, 'x2': 10, 'y2': 9},
{'x1': 7, 'y1': 2, 'x2': 10, 'y2': 1},
{'x1': 7, 'y1': 6, 'x2': 10, 'y2': 5},
{'x1': 7, 'y1': 10, 'x2': 10, 'y2': 9},
{'x1': 7, 'y1': 4, 'x2': 10, 'y2': 3},
{'x1': 7, 'y1': 8, 'x2': 10, 'y2': 7},
{'x1': 7, 'y1': 2, 'x2': 10, 'y2': 3},
{'x1': 7, 'y1': 6, 'x2': 10, 'y2': 7},
{'x1': 7, 'y1': 10, 'x2': 10, 'y2': 11},
{'x1': 9, 'y1': 1, 'x2': 8, 'y2': 4},
{'x1': 9, 'y1': 1, 'x2': 10, 'y2': 4},
{'x1': 9, 'y1': 5, 'x2': 8, 'y2': 8},
{'x1': 9, 'y1': 5, 'x2': 10, 'y2': 8},
{'x1': 9, 'y1': 9, 'x2': 8, 'y2': 12},
{'x1': 9, 'y1': 9, 'x2': 10, 'y2': 12},
{'x1': 9, 'y1': 7, 'x2': 8, 'y2': 4},
{'x1': 9, 'y1': 7, 'x2': 10, 'y2': 4},
{'x1': 9, 'y1': 5, 'x2': 8, 'y2': 2},
{'x1': 9, 'y1': 5, 'x2': 10, 'y2': 2},
{'x1': 9, 'y1': 9, 'x2': 8, 'y2': 6},
{'x1': 9, 'y1': 9, 'x2': 10, 'y2': 6},
{'x1': 9, 'y1': 3, 'x2': 8, 'y2': 6},
{'x1': 9, 'y1': 3, 'x2': 10, 'y2': 6},
{'x1': 9, 'y1': 7, 'x2': 8, 'y2': 10},
{'x1': 9, 'y1': 7, 'x2': 10, 'y2': 10},
{'x1': 9, 'y1': 4, 'x2': 8, 'y2': 1},
{'x1': 9, 'y1': 4, 'x2': 10, 'y2': 1},
{'x1': 9, 'y1': 8, 'x2': 8, 'y2': 5},
{'x1': 9, 'y1': 8, 'x2': 10, 'y2': 5},
{'x1': 9, 'y1': 2, 'x2': 8, 'y2': 5},
{'x1': 9, 'y1': 2, 'x2': 10, 'y2': 5},
{'x1': 9, 'y1': 6, 'x2': 8, 'y2': 9},
{'x1': 9, 'y1': 6, 'x2': 10, 'y2': 9},
{'x1': 9, 'y1': 10, 'x2': 8, 'y2': 13},
{'x1': 9, 'y1': 10, 'x2': 10, 'y2': 13},
{'x1': 9, 'y1': 4, 'x2': 8, 'y2': 7},
{'x1': 9, 'y1': 4, 'x2': 10, 'y2': 7},
{'x1': 9, 'y1': 8, 'x2': 8, 'y2': 11},
{'x1': 9, 'y1': 8, 'x2': 10, 'y2': 11},
{'x1': 9, 'y1': 6, 'x2': 8, 'y2': 3},
{'x1': 9, 'y1': 6, 'x2': 10, 'y2': 3},
{'x1': 9, 'y1': 10, 'x2': 8, 'y2': 7},
{'x1': 9, 'y1': 10, 'x2': 10, 'y2': 7}]
Upvotes: 1