8

Google or-tools のサンプルの 1 つは、n-queens 問題のソルバーです。 下部には、対称性を破る制約を制約ソルバーに追加することで実装を改善できることが示されています。

インターネットを見回すと、対称性が n-queens 問題の制約を破っていることがわかりましたが、それらを制約に変換して、それらを実装する 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-queens 問題の対称性の破れの制約を以下に示します。それらは、2 番目の段落のリンクから直接取得されます。

n クイーンの対称性の破れの制約

これらの制約がどのように機能するかを理解しています。この関数を n-queens ボードの各セルに適用して、状態を同等の状態に変換できるという考え方です。これらの状態の 1 つが、その状態の正規表現になります。これは、重複した評価を排除することによって、将来の処理を削減する方法として使用されます。

事後的にこれを実装するだけなら、上記で説明したことを正確に実行し、考えられる対称性を破る関数をそれぞれ使用して状態を変換し、ある種の状態ハッシュ (たとえば、各列で選択された行の文字列) を計算します。提案されたソリューションごとに最も低いものを選択します。以前に見たものについては、将来の処理をスキップします。

私の問題は、これらの変換を 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)]
4

2 に答える 2

2

カスタムの 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

于 2017-09-22T17:34:47.913 に答える