問題タブ [latin-square]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
algorithm - 超高層ビル (高さの手がかりのあるラテン語の正方形) を SAT に縮小する方法
超高層ビルのラテン方陣問題から SAT への縮小を実装しようとしています。
超高層ビルの問題は、Latin-sqaureと同じですが、さらに、超高層ビルのパズルでは、グリッドの端にある手がかりを満たすために、さまざまなユニークな高さの建物をグリッドに配置する必要があります。これらの「エッジの手がかり」は、ボードの端に沿って与えられた手がかりの配置の観点から、いくつの建物が見えるかをプレーヤーに伝えます。(完全な説明)
そこで、SAT ソルバーを使用してこの問題を解決するために、SAT を使用して suduko を解決する同様のアプローチを試みました (既に実行済みです)。最初に、n^3 バイナリ変数 X_i,j,k を定義しました。これは、i,j セルで値 k が true であることを示します (したがって、i,j セルには高さ k のスカイスクラッパーがあります)。
次の制約を CNF の形式で追加しました。
- 各セルには真の変数が 1 つだけ含まれます
- 各行には各値が 1 つだけ含まれます
- 各列には正確に各値が 1 つ含まれます
現在、手がかりと高さにどの制約を追加する必要があるかを判断するのに苦労しています。最初に、与えられた手がかりごとに可能なすべての順序を追加するオプションについて考えました。たとえば、左から 3 つの高層ビル (n = 4) が見える場合、可能性は [[2 ,3 ,4, 1],[1 ,3,4,2]] でも全部で O(n!) になると思います...
ILP を使用して Suduko ソルバーを実装したので、ILP (整数線形計画法) を使用してこの問題を解決する方法について読みました。その方法を説明するこのリンクを見つけました。しかし、SATソルバーに適合するILPの状況で追加された高さのconstarintに相当するものをまだ見つけることができません。
どうもありがとう！