Игра Sat решатель для Lights Out - PullRequest
Новая
       76

Игра Sat решатель для Lights Out

0 голосов
/ 27 февраля 2019

У меня есть школьный проект, в котором я должен найти решения игры "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

Ответы [ 2 ]

0 голосов
/ 28 февраля 2019

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

0 голосов
/ 27 февраля 2019

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

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

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

...