Спутниковый решатель для игры Lights Out

У меня есть школьный проект, где я должен найти решения игры "Lights Out" ( https://en.wikipedia.org/wiki/Lights_Out_(game) ) с помощью SAT Solver, но у меня возникают проблемы при попытке установить конъюнктивную нормальную форму игры.

Игра состоит из сетки 5 на 5 огней. Нажатие на любой из индикаторов переключит его и четыре соседних индикатора. Цель головоломки - выключить все огни.

Как я пытался до сих пор:

Для сетки 3х3 (для начала) я установил 9 терминов (для каждой кнопки) таким образом:

C11 : загорается кнопка в позиции 1,1 C12 : загорается кнопка в позиции 1,2 C13 : загорается кнопка в позиции 1,3. [...]

Так как кнопка в позиции 1,1 гаснет, кнопки в позиции 1,2 и 2,1

Я сделал C11 => C12 и C21 кнопка в положении 1,2 горит гаснет кнопка в положении 1,1 и 1,3 и 2,2 Я сделал C12 => C11 и C13 и C22

и продолжил для другого:

C13 => C12 and C23
C21 => C11 and C22 and C31
C22 => C12 and C21 and C23 and C32
C23 => C13 and C22 and C33
C31 => C21 and C32
C32 => C31 and C33 and C22
C33 => C23 and C32

затем я просто преобразовал их в CNF, чтобы получить пункты, которые мне нужны для спутникового решателя, но кажется, что я сделал что-то неправильно.

Может ли кто-нибудь помочь мне написать эту игру в форме CNF?

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

Вот игра, если вам нужно понять ее лучше:

https://www.geogebra.org/m/JexnDJpt#material/KArehWn8


logic solver sat satisfiability cnf
person johanDa9u    schedule 27.02.2019    source источник

Ответы (2)


arrow_upward
2
arrow_downward

В опубликованной вами статье в Википедии цитируется довольно хорошее решение: Марлоу Андерсон, Тодд Фейл (1998). «Выключение света с помощью линейной алгебры» (PDF) . Математический журнал. 71 (4): 300–303. Вам нужно будет понять математику в статье и то, как кодировать операции Z_2 в CNF. (ИМО меньше усилий по внедрению, чем BMC.) Желаем удачи в задании!

person Tim    schedule 27.02.2019

arrow_upward
1
arrow_downward

Один из способов решения проблемы — закодировать последовательность действий, необходимых для достижения цели.

Один из способов сделать это — считать, что для решения головоломки требуется K ходов. Затем вы будете кодировать для каждого шага выбранную ячейку и влияние на связанные ячейки, а также запрашивать у решателя модель, при которой в K-й конфигурации все индикаторы выключены.

Этот метод называется проверкой ограниченной модели, и вы должны найти несколько объяснений того, как преобразовать его в sat.

person Marco    schedule 27.02.2019