我是SAT解算器世界的新手,并且需要有关以下问题的一些指导。
考虑:
❶我选择了4 * 4网格中的14个相邻单元格
❷我有4个,2个,5个,2个和1个大小的5 polyominoes(A,B,C,D,E)
❸这些多氨基酸是免费,即它们的形状不固定,可以形成不同的图案
如何使用SAT求解器(最好是OR工具)在选定区域(灰色单元格)内计算这5个游离多氨基酸的所有可能组合
借用@spinkus的有深刻见解的答案和OR工具文档,我可以编写以下示例代码(在Jupyter Notebook中运行):
from ortools.sat.python import cp_model
import numpy as np
import more_itertools as mit
import matplotlib.pyplot as plt
%matplotlib inline
W, H = 4, 4 #Dimensions of grid
sizes = (4, 2, 5, 2, 1) #Size of each polyomino
labels = np.arange(len(sizes)) #Label of each polyomino
colors = ('#FA5454', '#21D3B6', '#3384FA', '#FFD256', '#62ECFA')
cdict = dict(zip(labels, colors)) #Color dictionnary for plotting
inactiveCells = (0, 1) #Indices of disabled cells (in 1D)
activeCells = set(np.arange(W*H)).difference(inactiveCells) #Cells where polyominoes can be fitted
ranges = [(next(g), list(g)[-1]) for g in mit.consecutive_groups(activeCells)] #All intervals in the stack of active cells
def main():
model = cp_model.CpModel()
#Create an Int var for each cell of each polyomino constrained to be within Width and Height of grid.
pminos = [[] for s in sizes]
for idx, s in enumerate(sizes):
for i in range(s):
pminos[idx].append([model.NewIntVar(0, W-1, 'p%i'%idx + 'c%i'%i + 'x'), model.NewIntVar(0, H-1, 'p%i'%idx + 'c%i'%i + 'y')])
#Define the shapes by constraining the cells relative to each other
## 1st polyomino -> tetromino ##
# #
# #
# # #
# ### #
# #
################################
p0 = pminos[0]
model.Add(p0[1][0] == p0[0][0] + 1) #'x' of 2nd cell == 'x' of 1st cell + 1
model.Add(p0[2][0] == p0[1][0] + 1) #'x' of 3rd cell == 'x' of 2nd cell + 1
model.Add(p0[3][0] == p0[0][0] + 1) #'x' of 4th cell == 'x' of 1st cell + 1
model.Add(p0[1][1] == p0[0][1]) #'y' of 2nd cell = 'y' of 1st cell
model.Add(p0[2][1] == p0[1][1]) #'y' of 3rd cell = 'y' of 2nd cell
model.Add(p0[3][1] == p0[1][1] - 1) #'y' of 3rd cell = 'y' of 2nd cell - 1
## 2nd polyomino -> domino ##
# #
# #
# # #
# # #
# #
#############################
p1 = pminos[1]
model.Add(p1[1][0] == p1[0][0])
model.Add(p1[1][1] == p1[0][1] + 1)
## 3rd polyomino -> pentomino ##
# #
# ## #
# ## #
# # #
# #
################################
p2 = pminos[2]
model.Add(p2[1][0] == p2[0][0] + 1)
model.Add(p2[2][0] == p2[0][0])
model.Add(p2[3][0] == p2[0][0] + 1)
model.Add(p2[4][0] == p2[0][0])
model.Add(p2[1][1] == p2[0][1])
model.Add(p2[2][1] == p2[0][1] + 1)
model.Add(p2[3][1] == p2[0][1] + 1)
model.Add(p2[4][1] == p2[0][1] + 2)
## 4th polyomino -> domino ##
# #
# #
# # #
# # #
# #
#############################
p3 = pminos[3]
model.Add(p3[1][0] == p3[0][0])
model.Add(p3[1][1] == p3[0][1] + 1)
## 5th polyomino -> monomino ##
# #
# #
# # #
# #
# #
###############################
#No constraints because 1 cell only
#No blocks can overlap:
block_addresses = []
n = 0
for p in pminos:
for c in p:
n += 1
block_address = model.NewIntVarFromDomain(cp_model.Domain.FromIntervals(ranges),'%i' % n)
model.Add(c[0] + c[1] * W == block_address)
block_addresses.append(block_address)
model.AddAllDifferent(block_addresses)
#Solve and print solutions as we find them
solver = cp_model.CpSolver()
solution_printer = SolutionPrinter(pminos)
status = solver.SearchForAllSolutions(model, solution_printer)
print('Status = %s' % solver.StatusName(status))
print('Number of solutions found: %i' % solution_printer.count)
class SolutionPrinter(cp_model.CpSolverSolutionCallback):
''' Print a solution. '''
def __init__(self, variables):
cp_model.CpSolverSolutionCallback.__init__(self)
self.variables = variables
self.count = 0
def on_solution_callback(self):
self.count += 1
plt.figure(figsize = (2, 2))
plt.grid(True)
plt.axis([0,W,H,0])
plt.yticks(np.arange(0, H, 1.0))
plt.xticks(np.arange(0, W, 1.0))
for i, p in enumerate(self.variables):
for c in p:
x = self.Value(c[0])
y = self.Value(c[1])
rect = plt.Rectangle((x, y), 1, 1, fc = cdict[i])
plt.gca().add_patch(rect)
for i in inactiveCells:
x = i%W
y = i//W
rect = plt.Rectangle((x, y), 1, 1, fc = 'None', hatch = '///')
plt.gca().add_patch(rect)
问题是我已经硬编码了5个唯一/固定的多米诺骨牌,但我不知道如何定义约束,以便考虑到每个多米诺骨牌的每种可能模式(只要有可能)。
对于每个polyonomino和每个可能的左上角单元格,都有一个布尔变量,指示该单元格是否是封闭矩形的左上角部分。
对于每个单元格和每个多义胺,您都有一个布尔变量,指示该单元格是否被该多义胺占据。
现在,对于每个单元格和每个多米诺骨牌,都有一系列含义:选择左上角的单元格意味着每个单元格实际上都被该多米诺骨牌占据。
然后限制:每一个细胞最多可容纳一个多胺对于每个多米诺骨牌,它的左上部分正好有一个单元格。
这是一个布尔值问题。
是的,您可以使用OR-Tools中的constraint programming完成。 OR-Tools对2D网格几何形状一无所知,因此您必须根据位置约束对每个形状的几何形状进行编码。即形状是块/单元的集合,这些块/单元必须彼此具有一定的关系,必须在网格的范围内并且不能重叠。一旦有了约束模型,您就可以要求CP-SAT Solver解决所有可能的解决方案。
这是一个非常简单的概念证明,在4x4网格上具有两个矩形形状(您可能还想添加某种解释器代码,以便从形状描述转到一组OR-Tools变量和更大的约束中规模问题,因为手动输入约束有点乏味。]
from ortools.sat.python import cp_model
(W, H) = (3, 3) # Width and height of our grid.
(X, Y) = (0, 1) # Convenience constants.
def main():
model = cp_model.CpModel()
# Create an Int var for each block of each shape constrained to be within width and height of grid.
shapes = [
[
[ model.NewIntVar(0, W, 's1b1_x'), model.NewIntVar(0, H, 's1b1_y') ],
[ model.NewIntVar(0, W, 's1b2_x'), model.NewIntVar(0, H, 's1b2_y') ],
[ model.NewIntVar(0, W, 's1b3_x'), model.NewIntVar(0, H, 's1b3_y') ],
],
[
[ model.NewIntVar(0, W, 's2b1_x'), model.NewIntVar(0, H, 's2b1_y') ],
[ model.NewIntVar(0, W, 's2b2_x'), model.NewIntVar(0, H, 's2b2_y') ],
]
]
# Define the shapes by constraining the blocks relative to each other.
# 3x1 rectangle:
s0 = shapes[0]
model.Add(s0[0][Y] == s0[1][Y])
model.Add(s0[0][Y] == s0[2][Y])
model.Add(s0[0][X] == s0[1][X] - 1)
model.Add(s0[0][X] == s0[2][X] - 2)
# 1x2 rectangle:
s1 = shapes[1]
model.Add(s1[0][X] == s1[1][X])
model.Add(s1[0][Y] == s1[1][Y] - 1)
# No blocks can overlap:
block_addresses = []
for i, block in enumerate(blocks(shapes)):
block_address = model.NewIntVar(0, (W+1)*(H+1), 'b%d' % (i,))
model.Add(block[X] + (H+1)*block[Y] == block_address)
block_addresses.append(block_address)
model.AddAllDifferent(block_addresses)
# Solve and print solutions as we find them
solver = cp_model.CpSolver()
solution_printer = SolutionPrinter(shapes)
status = solver.SearchForAllSolutions(model, solution_printer)
print('Status = %s' % solver.StatusName(status))
print('Number of solutions found: %i' % solution_printer.count)
def blocks(shapes):
''' Helper to enumerate all blocks. '''
for shape in shapes:
for block in shape:
yield block
class SolutionPrinter(cp_model.CpSolverSolutionCallback):
''' Print a solution. '''
def __init__(self, variables):
cp_model.CpSolverSolutionCallback.__init__(self)
self.variables = variables
self.count = 0
def on_solution_callback(self):
self.count += 1
solution = [(self.Value(block[X]), self.Value(block[Y])) for shape in self.variables for block in shape]
print((W+3)*'-')
for y in range(0, H+1):
print('|' + ''.join(['#' if (x,y) in solution else ' ' for x in range(0, W+1)]) + '|')
print((W+3)*'-')
if __name__ == '__main__':
main()
Gives:
...
------
| |
| ###|
| # |
| # |
------
------
| |
| ###|
| # |
| # |
------
------
| |
| ###|
| #|
| #|
------
Status = OPTIMAL
Number of solutions found: 60