Вы хотите найти два разных решения для одного и того же японского кроссворда?
По-хорошему тут нужна некая внешняя валидация. Когда выхлоп от SAT-решателя обрабатывается и сравнивается с известным решением для этого кроссворда. Всегда есть вероятность, что решатель случайно попал в правильное решение, просто потому что в задаче может быть огромное число переменных и он что-то там подобрал, чтобы сделать КНФ истинной, но начальные условия оставляют ровно один вариант, если всё-таки нашлось какое-то другое решение и кодировка 100% правильная, то значит плохой решатель.
Не сочтите меня грубияном, но при наличии хорошего текстового описания алгоритма, я должен быть в состоянии написать код сам. А в том, что написано у вас я всё ещё мало что понял.
В пункте 2 вы меня убедили, был невнимателен. Если вы не против несколько вопросов про пункт 1. Блок это несколько закрашенных клеток подряд? Переменные X1...XN это все клетки строки или столбца? Каким образом формула из первого шага связана с конкретным блоком?
Вы простите меня, но я попробовал вчитаться, появились вопросы к вашему алгоритму, было бы круто, если бы был ещё пример кодирования японского кроссворда по вашему алгоритму.
Самое первое — фактически вы работаете с матрицей n*m, а у всех переменных по одному индексу. Понятно, что в формулах подразумеваются именно переменные из уже готовой SAT кодировки, но формулы воспринимаются очень трудно.
Не понятно что скрывается за словом «блок», для человека не решавшего японские кроссворды, смутно припоминаю, что цифрами на полях задаётся число закрашенных клеток подряд ну и собственно порядок таких последовательностей. А какой смысл вкладывается в это понятие в смысле SAT кодировки?
Второе условие вообще не должно оказывать никакого влияния на количество появлений «блока», потому что это дизъюнкт. Допустим у нас три возможных позиции блока, пусть им соответствуют переменные с номерами 1, 2, 3. Если блок может стоять в позициях 1 и 2(соответственно они истины, а 3 ложная), то по формуле два получим -1V-2V-3, это можно переписать как (false V false V true == true). Получается, что единственный вариант, когда это «ограничение» сыграет, это ситуация, когда блок может стоять где угодно. Для подобных ограничений лучше использовать XOR, это я по своему опыту говорю.
То же самое про шаг 3, он ничего не ограничивает.
В шагах 4 и 5 я вообще ничего не понял.
Не имея «на руках» доказательств решения этих кроссвордов, я могу говорить, что что-то у вас там находится, но в ряд ли это то, что надо.
Клоз == дизъюнкт. Второй вариант всё-таки как-то лучше звучит. Да и в дискретке вы не найдете термина «клоз».
Как уже выше отмечали — неплохо бы привести результат. Выполняющий набор для какого-нибудь небольшого примера. Циферки-то может и красивые, а вот что за ними прячется не ясно.
Каюсь, поторопился с комментарием, полез смотреть этот самый PEP, до этого был не в курсе, испугался, что сделали из питона паскаль с этим его :=, но потом вчитался и теперь не понимаю из-за чего весь сыр бор, в отдельных ситуациях жизнеспособная конструкция.
Аппараты для проверки подлинности паспорта есть и в сбере активно используются, пару недель назад выпускал себе Моментум, так когда даёшь паспорт сотрудники сначала смотрят сличают фото и человека, а потом каждую страницу паспорта смотрят в этой вот машине.
Рекламная статья или нет это я оставлю на совести автора, но вот как он смог играть в Асфальт 8 в 2010 году, если вышел он в 2013, а на bada os вообще не выходила?
А почему нельзя было взять юсб-клавиатуру, и на её основе сделать то же самое, только ограничение на количество кнопок было бы уже не столь жесткое, при необходимости можно было бы даже добавить что-то новое. А вообще, конечно, вы хороший внук.
Лично у меня первая мысль была повесить на кота ошейник с чем-то типа RFID метки, и поставить считыватель, который уже запрограммировать на разного рода оповещения.
По-хорошему тут нужна некая внешняя валидация. Когда выхлоп от SAT-решателя обрабатывается и сравнивается с известным решением для этого кроссворда. Всегда есть вероятность, что решатель случайно попал в правильное решение, просто потому что в задаче может быть огромное число переменных и он что-то там подобрал, чтобы сделать КНФ истинной, но начальные условия оставляют ровно один вариант, если всё-таки нашлось какое-то другое решение и кодировка 100% правильная, то значит плохой решатель.
В пункте 2 вы меня убедили, был невнимателен. Если вы не против несколько вопросов про пункт 1. Блок это несколько закрашенных клеток подряд? Переменные X1...XN это все клетки строки или столбца? Каким образом формула из первого шага связана с конкретным блоком?
Самое первое — фактически вы работаете с матрицей n*m, а у всех переменных по одному индексу. Понятно, что в формулах подразумеваются именно переменные из уже готовой SAT кодировки, но формулы воспринимаются очень трудно.
Не понятно что скрывается за словом «блок», для человека не решавшего японские кроссворды, смутно припоминаю, что цифрами на полях задаётся число закрашенных клеток подряд ну и собственно порядок таких последовательностей. А какой смысл вкладывается в это понятие в смысле SAT кодировки?
Второе условие вообще не должно оказывать никакого влияния на количество появлений «блока», потому что это дизъюнкт. Допустим у нас три возможных позиции блока, пусть им соответствуют переменные с номерами 1, 2, 3. Если блок может стоять в позициях 1 и 2(соответственно они истины, а 3 ложная), то по формуле два получим -1V-2V-3, это можно переписать как (false V false V true == true). Получается, что единственный вариант, когда это «ограничение» сыграет, это ситуация, когда блок может стоять где угодно. Для подобных ограничений лучше использовать XOR, это я по своему опыту говорю.
То же самое про шаг 3, он ничего не ограничивает.
В шагах 4 и 5 я вообще ничего не понял.
Не имея «на руках» доказательств решения этих кроссвордов, я могу говорить, что что-то у вас там находится, но в ряд ли это то, что надо.
Как уже выше отмечали — неплохо бы привести результат. Выполняющий набор для какого-нибудь небольшого примера. Циферки-то может и красивые, а вот что за ними прячется не ясно.