我正在研究BDD的应用程序,以确定是否可以在那里实现x,y概念。
让我解释一下。
比方说,我有z,分布在x,y坐标平面上。限制条件是:
- 所有z项都必须放置在x,y坐标平面中
- z中的一些项目必须彼此相距一定距离
我认为整数线性规划可以解决这个问题。例如,通过一组方程,我可以表示上面的约束,并进行线性规划来求解精确的位置。
但我想问的是BDD是否可以帮助解决这个问题?
换句话说,二进制决策图能代表x,y坐标吗?我能用布尔函数(相当于上面的方程组(和BDD来表示上述约束吗?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}]