Способ приведения небоскреба (латинского квадрата с указанием высоты) к SAT

Question

Я пытаюсь реализовать сокращение от латинского квадрата задачи небоскреба до SAT.

Проблема небоскреба такая же, как у Latin-sqaure , но, кроме того, загадка небоскреба просит игрока разместить на сетке здания разной и уникальной высоты, чтобы они соответствовали подсказкам, указанным на краях сетки. Эти «подсказки по краям» говорят игроку, сколько зданий видно с точки зрения размещения данного ключа по краю доски. ( полное объяснение )

Поэтому, чтобы решить эту проблему с помощью SAT-решателя, я попробовал аналогичный подход к решению suduko с использованием SAT (что я уже сделал). Итак, прежде всего я определил n ^ 3 двоичных переменных, X_i, j, k, которые указывают, что в ячейке i, j значение k истинно (поэтому в ячейке i, j у нас есть небоскреб с высотой k)

Я добавил следующие ограничения в форме CNF:

1. каждая ячейка содержит только 1 истинную переменную
2. каждая строка содержит ровно 1 каждого значения
3. каждый столбец содержит ровно 1 каждого значения

Теперь у меня возникают проблемы с выяснением, какие ограничения я должен добавить для подсказок и высот. Сначала я подумал о возможности добавления каждого возможного ордера для каждой данной подсказки, например, если слева я вижу 3 небоскреба (n = 4), то есть возможности: [[2, 3, 4, 1], [1 , 3,4,2]], но я думаю, что в целом это будет O (n!) ...

Я реализовал решатель Suduko с использованием ILP, поэтому я прочитал об решении этой проблемы с помощью ILP (целочисленное линейное программирование) , Я нашел эту ссылку , которая описывает, как это сделать. Но все же я не могу найти эквивалент для ограничения высоты, который они добавили в ситуации ILP, который бы подходил для решателя SAT.

Большое спасибо!

Answer 1

Вероятно, существует множество подходов, но один из них может выглядеть следующим образом:

Для каждой подсказки C_i вы вводите новые вспомогательные переменные:

# NV_?_j = position j is not visible (in regards to clue i)

NV_i_1, NV_i_2, ... NV_i_n  

Подсказка состоит в том, чтобы указать правильную мощность (различные подходы; вы выбрали как)

sum(NV_1_?) = clue-hint(C_1)

Теперь вопрос состоит в том, как ограничить NV:

• NV_i_1 = true всегда действительный
• NV_i_j = true <-> there exists a HIGHER value EARLIER

Это быстро растет, но я рекомендую следующий подход (который не должен быть проблемой для тех размеров, которые я видел на ваших связанных страницах; хотя SAT является менее естественный подход, чем, например, CP):

Для N=5, ограниченного вашим ограничением для всех различий, есть C(N, 2) = 10 уникальных пар без симметрии:

1 2    2 3    3 4    4 5
1 3    2 4    3 5
1 4    2 5  
1 5

You теперь будут использовать эти пары в отношении:

• парных позиций (1 - N)
• парных значений (1 - N)

Предполагая, что ваш переменные решения - это тензор некоторого тензора ранга 3 (позиция строки, позиция столбца, значение в унарной кодировке) с размерами (N, N, N):

X111 = row = 1 | column = 1 | value = 1
X112 = row = 1 | column = 1 | value = 2
...
X121 = row = 1 | column = 2 | value = 1
... 

NV_i_j = true <-> there exists a HIGHER value EARLIER можно выразить как (мы предполагаем, что ключ активен в некотором столбце здесь):

NV_i_1 <-> true  # fact

# pairs compared: position 1 2
NV_i_2 <-> (X115 ^ X124) | (X115 ^ X123) | ...  | (x112 ^ X121)

# pairs compared: position 1 3 + position 2 3
# 3 compared to 1 and 2 -> existence of HIGHER value EARLIER (2 positions)
NV_i_3 <-> (X115 ^ X134) | (X115 ^ X133) | ...  | (x112 ^ X131) |
           (X125 ^ X134) | (X125 ^ X133) | ...  | (x122 ^ X131) 

...

# pairs compared: position 1 5 + position 2 5 + position 3 5 + position 4 5 
NV_i_5 <-> (X115 ^ X154) | (X115 ^ X153) | ...  | (x112 ^ X151) |
           (X125 ^ X154) | (X125 ^ X153) | ...  | (x122 ^ X151)
           ...
           (X145 ^ X154) | (X145 ^ X153) | ...  | (x142 ^ X151)

Теперь осталась только одна вещь (и я не буду это показывать):

• преобразование этих компонентов в cnf
  • вы уже сделали некоторую кардинальную кодировку для вашего all-diff разложения
    • можно использовать повторно для количества элементов, необходимых для подсказок
  • для NV ограничения:
    • я рекомендую использовать внешние инструменты (sympy, mathematica, ...) вместо того, чтобы делать это вручную
    • я также рекомендую передать это в некоторые функции который передается чем-то вроде подматрицы вашего тензора (тензора, где строка или столбец, где активна подсказка, отщепляется) + clue_n