N皇后问题对称性破解之Google OR工具

Question

Google or-tools的样例之一是用于n皇后问题的求解器。底部指出，通过向约束求解器添加对称性破坏约束可以改善实现。

我在互联网上搜索到了关于N皇后问题对称性破缺的限制条件，但我无法想象如何将这些限制条件转换为实现它们的Python代码。

---

编辑：这是一个不好的问题，让我们更新...

我尝试了什么？

这是来自上面第一个链接的设置：

from ortools.constraint_solver import pywrapcp

N = 8
solver = pywrapcp.Solver("n-queens")
# Creates the variables.
# The array index is the column, and the value is the row.
queens = [solver.IntVar(0, N - 1, "x%i" % i) for i in range(N)]
# Creates the constraints.
# All rows must be different.
solver.Add(solver.AllDifferent(queens))
# All columns must be different because the indices of queens are all different.
# No two queens can be on the same diagonal.
solver.Add(solver.AllDifferent([queens[i] + i for i in range(N)]))
solver.Add(solver.AllDifferent([queens[i] - i for i in range(N)]))

# TODO: add symmetry breaking constraints

db = solver.Phase(queens, solver.CHOOSE_FIRST_UNBOUND, solver.ASSIGN_MIN_VALUE)
solver.NewSearch(db)
num_solutions = 0
while solver.NextSolution():
  num_solutions += 1
solver.EndSearch()
print()
print("Solutions found:", num_solutions)
print("Time:", solver.WallTime(), "ms")

我知道我可以成功地实现简单的约束。如果我想要确保解决方案总是在第一行的第一列有一个皇后，我可以像这样实现：

solver.Add(queens[0] == 0)

queens[0]变量表示皇后在第一列的位置，只有当第一列的第一行有一个皇后时，才满足此约束条件。当然，这并不是我想要做的，因为可能存在解决方案不包括任何角落单元格。

n-皇后问题的对称性破坏约束如下所示。它们直接从第二段中的链接中提取。

我了解这些约束条件的工作原理。想法是，您可以将此函数应用于n皇后棋盘上的每个单元格，以将状态转换为等效状态。其中一个状态将是该状态的规范表示。这被用作通过消除重复评估来修剪未来处理的方法。

如果我只是事后实现它，我会按照上述描述的方式进行，使用每个可能的对称性破坏函数转换状态，计算某种状态哈希（例如，每列中选定行的字符串），并选择每个提议解决方案的最低解决方案。跳过我们以前见过的未来处理。

我的问题是，我不知道如何将这些转换转换为google or-tools约束编程求解器的约束条件。

让我们看看最简单的一个，d1（r [i] = j）=> r [j] = i，即关于主对角线的反射。我知道需要将变换应用于所有单元格，然后与当前状态进行比较，以防止其被扩展。我不了解足够的Python知识来了解在此处适用于变换的表达式类型，而且我无法弄清楚如何创建用于此特定求解器的约束，以将变换与当前状态进行比较。

state = [queens[i].Value() for i in range(N)]
symX    = [state[N - (i + 1)] for i in range(N)]
symY    = [N - (state[i] + 1) for i in range(N)]
symD1   = [state.index(i) for i in range(N)]
symD2   = [N - (state.index(N-(i+1)) + 1) for i in range(N)]
symR90  = [N - (state.index(i) + 1) for i in range(N)]
symR180 = [N - (state[N-(i+1)] + 1) for i in range(N)]
symR270 = [state.index(N-(i+1)) for i in range(N)]

- Nick Larsen

Answer 1

我尝试使用自定义的DecisionBuilder来利用对称性作为新的约束条件来修剪搜索树，但是我无法使其正常工作。

相反，我必须使用一个SearchMonitor来捕获每个解决方案的事件，并检查该解决方案是否是先前解决方案的对称形式。

下面是SearchMonitor的代码，覆盖“AcceptSolution”函数的解决方案捕获以及gen_symetries函数来计算和检查所有可能的对称形式。

    class SearchMonitor(pywrapcp.SearchMonitor):
    def __init__(self, solver, q):
        pywrapcp.SearchMonitor.__init__(self, solver)
        self.q = q
        self.all_solutions = []
        self.unique_solutions = []
        self.n = len(self.q)

    def AcceptSolution(self):
        qval = [self.q[i].Value() for i in range(self.n)]
        self.all_solutions.append(qval)

        symmetries = [vv in self.unique_solutions for vv in gen_symmetries(self.n, qval)]

        if sum(symmetries) == 0:
            self.unique_solutions.append(qval)

        return False

def gen_symmetries(n, solution):
    symmetries = []

    #x(r[i]=j) → r[n−i+1]=j
    x = list(range(n))
    for index in range(n):
        x[n - 1 - index] = solution[index]

    symmetries.append(x)

    #y(r[i]=j) → r[i]=n−j+1
    y = list(range(n))
    for index in range(n):
        y[index] = (n - 1 - solution[index])

    symmetries.append(y)

    #d1(r[i]=j) → r[j]=i
    d1 = list(range(n))
    for index in range(n):
        d1[solution[index]] = index

    symmetries.append(d1)

    # d2(r[i]=j) → r[n−j+1]=n−i+1
    d2 = list(range(n))
    for index in range(n):
        d2[n - 1 - solution[index]] = (n - 1 - index)

    symmetries.append(d2)

    # r90(r[i]=j) → r[j] = n−i+1
    r90 = list(range(n))
    for index in range(n):
        r90[solution[index]] = (n - 1 - index)

    symmetries.append(r90)

    # r180(r[i]=j) → r[n−i+1]=n−j+1
    r180 = list(range(n))
    for index in range(n):
        r180[n - 1 - index] = (n - 1 - solution[index])

    symmetries.append(r180)

    # r270(r[i]=j) → r[n−j+1]=i
    r270 = list(range(n))
    for index in range(n):
        r270[n - 1 - solution[index]] = index

    symmetries.append(r270)

    return symmetries

稍后你只需像这样将监视器添加到你的求解器中即可。

monitor = SearchMonitor(solver, queens)
solver.Solve(db, monitor)
solver.NewSearch(db)

最后只需打印出所有唯一解决方案即可。

print("Unique Solutions:", len(monitor.unique_solutions), monitor.unique_solutions)

您可以在gist中看到完整的工作示例。 https://gist.github.com/carlgira/7a4e6cf0f7b7412762171015917bccb4

- Carlos Giraldo

Answer 2

你必须利用已知的解对称关系来识别约束条件，以消除等效解。

1. 对于每个满足 queens[0] >= N/2 的解，都有一个垂直镜像的解满足 queens[0] <= N/2。因此，我们可以寻找 queens[0] 值更小的解，并添加以下约束：

   solver.Add(queens[0] < (N+1)//2) # 处理 N 的奇偶值
   

2. 然后，满足条件 queens[0] < queens[N-1] 的解与一个水平镜像的解等价，该解满足 queens[0] > queens[N-1]。您可以告诉求解器仅查找左侧列中的皇后在右侧列中的皇后下方的解：

   solver.Add(queens[0] < queens[N-1])
   

我无法轻易地制定一个反映旋转对称性的约束条件，但我相信这是可能的。

- Leon