我正在研究 BDD 的应用，以确定是否可以在那里实现 x,y 概念。
让我解释。
假设我有 z 的东西要分布在 x,y 坐标平面上。约束是：
我认为整数线性规划可以解决这个问题。例如，使用一组方程，我可以表示上述约束并进行线性规划以求解确切位置。
但我要问的是 BDD 是否可以帮助解决这个问题？
换句话说，二元决策图可以表示 x,y 坐标吗？我可以用布尔函数（相当于上面的方程组）来表示上述约束，并且可以操纵 BDD 来解决上述精确位置的约束，就像线性规划一样？
我没有任何具体的例子可以展示，但我认为用二进制表示等效的 x,y 坐标是一个起点？
是的，可以使用二元决策图对平面上给定的整数值问题进行编码，从而计算答案（作为令人满意的分配）。例如，使用 Python 包omega（它使用 Python 包dd进行 BDD 计算）：
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)
使用具有上述距离约束的 BDD 会导致变量数量呈指数级增长的 BDD。原因是表示乘法会导致指数大小的 BDD，如https://doi.org/10.1109/12.73590中所证明的那样。
如果约束不是点之间的距离，而是沿每个轴的距离（即，或 的绝对值或两者上的不等式或等式约束x1 - x2）y1 - y2，则避免了指数复杂性。
以上解决了网格上的放置问题。这是一个离散的放置问题。连续放置问题不能用二元决策图解决，因为它需要浮点运算。
上面的程序打印：
[{'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}]