zebra
1.0.0
Сегодня, в 2024 году, проект практически не поддерживается. Я использую его как площадку для некоторых вещей, которые хочу попробовать, но не рекомендую никому строить на его основе.
Помните логические головоломки, которые выглядели вот так? У них были такие подсказки:
Между Тушаром и Мауи есть один дом.
Любимая видеоигра Руби — «Покемоны».
Любителю чая не нравится синий цвет.
В детстве мне они нравились, и просмотр выступления Раймонда Хеттингера на PyCon 2019 вдохновил меня вернуться к этим проблемам. Он показал нам, как их решать; Я хотел научиться их генерировать.
Используя современный Python и решатели удовлетворения ограничений (SAT), этот проект можно использовать для создания случайных головоломок с зеброй.
В этом проекте используются Python 3.12 и Poetry.
Точка входа в этот проект — src/main.py ; соответственно, запустите его с помощью [poetry run] python -m src.main . Мы используем вопросник для создания интерфейса командной строки с простой интерактивностью.
Другие важные файлы:
puzzle.py содержит основной класс Puzzle, который в основном объединяет подсказки и элементы головоломки.
clues.py определяет подсказку (оператор более высокого уровня, который мы можем преобразовать в CNF) и несколько фабрик, таких как found_at или same_house ; generate.py есть утилиты для создания подсказок
elements.py и traptor_elements.py содержат различные элементы головоломки.
Наконец, sat_utils.py содержит основные утилиты для взаимодействия с решателем SAT pycosat. Этот код почти полностью был написан Раймондом Хеттингером для его выступления в 2019 году (спасибо!).
❯ поэзия запускает python -m src.main? Насколько велика головоломка? (Используйте клавиши со стрелками)
» 5
4
3? Выберите тип Траптора (используйте клавиши со стрелками)
? Тропический
» ? Мифический? ? Должен ли пазл включать в себя смузи? (Используйте клавиши со стрелками)
" Да
Нет? ? Должна ли головоломка включать крышки от бутылок? (Используйте клавиши со стрелками)
" Да
Нет
Подсказки
-----# ... Некоторый дополнительный текст опущен ...1. Малый Траптор и Болотный Траптор находятся в одном доме.
2. Древний ловец находится прямо слева от шоколадного смузи.
3. Древний Траптор и Лимонный коктейль находятся в одном доме.
4. Вулкан-Траптор находится прямо слева от Неугомонного Ловца.
5. Пещерный ловец и Зеленые крышки находятся в одном доме.
6. Между озером Траптор и Snapper Traptor есть два дома.
7. Зеленые пробки и Свирепый ловец находятся в одном доме.
8. Между Черными крышками и Кокосовым смузи есть один дом.
9. Между Малым Траптором и Киви-смузи есть один дом.
10. Dweller Traptor и Шоколадный смузи находятся в одном доме.
11. Красные пробки и Житель-ловушка находятся в одном доме.
12. Красные крышки от бутылок находятся прямо слева от Hoarder Traptor.
13. Между смузи Starfruit и желтыми крышками стоят два дома.
14. Озерный Траптор и Черные крышки находятся в одном доме.
15. Сталкер-Траптор и Свирепый Ловец находятся в одном доме.
Решение
┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━ ┳━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━ ━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━┓
┃ Гнездо ┃ Мифический ТрапторПервичный ┃ Мифический ТрапторВторичный ┃ Мифический ТрапторТретичный ┃ Смузи ┃ Крышка от бутылки ┃
┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━ ╇━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━ ━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━┩
│ 1 │ Свирепый ловец │ Пещерный ловец │ Сталкер-ловушка │ Смузи из карамболы │ Зеленые крышки от бутылок │
│ 2 │ Древний ловец │ Озерный ловец │ Ползучий ловец │ Лимонный смузи │ Черные крышки от бутылок │
│ 3 │ Малый ловец │ Болотный ловец │ Охотник-обитатель │ Шоколадный смузи │ Красные пробки │
│ 4 │ Большой ловец │ Вулкан-ловушка │ Охотник-накопитель │ Кокосовый коктейль │ Желтые крышки от бутылок │
│ 5 │ Неугомонный ловец │ Горный ловец │ Люциан-ловец │ коктейль «Киви» │ Синие крышки от бутылок │
└──────┴───────────────────────┴──────────────── ─────────┴────── ────────────────────┴────────────────────────┴──── ────────────────┘Что мне нужно сделать в феврале 2024 года, чтобы считать это «выполненным»?
Добавьте шаблоны HTML, потому что сайт, для которого я их создаю, требует включения таких вещей, как теги BR.
Улучшите грамматические особенности вывода, например, использование заглавных букв во вкусовом тексте.
Добавьте ресурсы верхнего и нижнего колонтитула, которые я копирую/вставляю в отправку.
Возможно, когда-нибудь я рассмотрю веб-интерфейс. Могу ли я реализовать проект с помощью пиодида, или пикосат на базе C вызовет проблемы? А как насчет другого интерфейса логического программирования, такого как PySAT, программирования набора ответов или других из этой темы HN?
Это может произойти. Но проект наконец-то достиг того уровня, которым я доволен, и поэтому я рад поделиться им и написать о нем.
18 февраля: сделайте вывод более простым, менее многословным и красивым. Обновите этот README, добавив новое форматирование и изменения. Наконец-то используйте генератор головоломок, чтобы создать новую головоломку!
17 февраля: обновите подпись головоломки, чтобы принимать только решение, выводя из него элементы и классы элементов. Добавьте более красивое отображение решения.
26.11: Почистите логику генерации головоломок/решений. Позвольте пользователю выбрать размер головоломки.
25.11. Назовите некоторые распространенные типы псевдонимами типов (спасибо, Python 3.12). Используйте регистрацию вместо распечаток.
Добавьте тесты для типов подсказок в generate.py .
Исправьте ошибку, которую я представил в clues.py . Этот файл очень сложно понять, но для него также сложно писать модульные тесты; конвертировать логические выражения в CNF вручную — неинтересное занятие.
Настройте веса подсказок в решении. Подготовьтесь к интеграции классов головоломок и решений.
Удалите флажок «Смузи» в виде флажка, потому что он только мешает быстро решать головоломки.
Продолжайте добавлять тесты. Завершите модульные тесты для sat_utils.py и начните пару тестов для clues.py , хотя этот файл очень сложно протестировать из-за сложности ручного вычисления преобразований DNF в CNF.
Следующие шаги — объединить головоломку и решение, создать лучший __repr__ и упростить представление размера головоломки (атрибут Puzzle , кортеж целых чисел от 1 до N, просто число n_houses и т. д.).
Удалите черный цвет и используйте ерш для форматирования. Обновите зависимости. Добавьте новый интерфейс командной строки с более простым и понятным использованием; python -m src.main .
Переименуйте SATLiteral -> PuzzleElement (смузи, кот и т. д.); это поясняет, что это не литерал в логическом смысле, а имя, например, для персонажей в головоломке.
Создайте новый тип SATLiteral (который представляет собой str в плаще); это представляет литерал в смысле логической переменной, например «Значение el находится в доме loc » или «Значение el не находится в доме loc ». Внутри они представлены некоторым целым числом i и его отрицательным аналогом -i .
Используйте (новый) SATLiteral в качестве типа возвращаемого значения comb(el: str, loc: int) -> SATLiteral , сопоставляя элементы головоломки с литералами, и neg(el: SATLiteral) -> SATLiteral для отрицания литерала.
Добавить Clause: tuple[SATLiteral, ...] представляющий «∨» (логическое ИЛИ; дизъюнкция) литералов; например, (1, -5, 6) — это дизъюнкция, утверждающая, что x_1 истинно, x_5 неверно или x_6 истинно.
Добавьте ClueCNF: list[Clause] , представляющий «∧» (логическое И; соединение) Clause s. Головоломка в CNF представляет собой «И из ИЛИ» («∧ из ∨s» или «∧ из предложений»).
Распечатайте головоломку более четко. Уменьшите детализацию сокращения подсказок.
Случайным образом создавайте головоломку (с семенем) при каждом запуске.
Переместите примеры в отдельные файлы. Обновление до Python 3.12 (бета). Добавьте больше правил lint. Очистите импорт.
Добавить инструменты разработчика (черный, ерш, пирайт); запустите black & ruff в предварительной фиксации. Обновите некоторые типы.
«∧» — это логическое И
«∨» — это логическое ИЛИ
Предложение — это «∨ литералов»
CNF — это «∧ предложений» или, что то же самое, «∧ из ∨» («И из ИЛИ»)
ДНФ, напротив, представляет собой «∨ из ∧s». DNF — это ответ на проблему SAT; DNF «A или B или C» означает, что A, B и C являются действительными (удовлетворяющими) назначениями. Таким образом, преобразование КНФ в ДНФ является NP-трудным, поскольку из ДНФ можно считать решения для КНФ.
CNF — это ∧ ∨s, где ∨ относится к переменным или их отрицаниям (литералам); ∨ литералов также называется предложением. ДНФ — это ∨ из ∧s; ∧ литералов называется термином.
Суть этого проекта заключается в том, чтобы выразить головоломку зебры как задачу булевой выполнимости (SAT) (Wikipedia.
Известно, что задача 3-SAT является NP-полной . То есть, вероятно, не существует алгоритма с полиномиальным временем для ее решения. Однако это описывает только общий случай.
Наша проблема маленькая и четко конкретизированная (ведь мы создаем их специально для людей!). Это делает его превосходным решением для современных решателей SAT, и доклад (и заметки) Хеттингера прекрасно это демонстрируют.
