Задача выполнимости булевых формул (SAT) 🧩 — определить, существует ли набор значений переменных, при котором все заданные логические выражения становятся истинными [1]. Если решение есть, следующая цель — перечислить все возможные варианты.
Знаменитую задачу о восьми ферзях (или её обобщение для N ферзей) можно решить, преобразовав её в булеву формулу и используя SAT-решатель ♟️.
Как начать? Шахматная доска — это сетка 8×8. Каждой клетке сопоставим переменную bij (i, j от 1 до 8), где bij = истина, если на клетке стоит ферзь.
Условия:
1️⃣ Каждая строка содержит ровно одного ферзя. Это включает два подусловия:
- Хотя бы один ферзь в строке: для строки i пишем дизъюнкцию bi1 ∨ bi2 ∨ … ∨ bi8 ✅.
- Не более одного ферзя в строке — тут сложнее ❗
Первый подход ➡️ Используем импликации. Например, если в первом столбце строки есть ферзь (b11), то в остальных его быть не должно:
b11 ⇒ ¬(b12 ∨ b13 ∨ … ∨ b18)
Преобразуем импликацию в дизъюнкцию: ¬b11 ∨ ¬b12 ∨ ¬b13 ∨ … ∨ ¬b18 🔄.
Второй подход 🤝 Для каждой пары клеток в строке добавляем условие: «либо в первой клетке нет ферзя, либо во второй». Для строки из 8 клеток получим 28 условий (комбинации пар):
(¬b11 ∨ ¬b12) ∧ (¬b11 ∨ ¬b13) ∧ … ∧ (¬b17 ∨ ¬b18)
Этот метод сразу даёт формулу в конъюнктивной нормальной форме (КНФ) 🧠 — «И» от множества «ИЛИ».
Аналогичные условия применяем для столбцов и диагоналей. После этого SAT-решатель найдёт все расстановки ферзей, удовлетворяющие правилам 👑.
Заметки 🔗
- Если формул несколько, их можно объединить через «И» в одну [1].
- Подробнее о SAT-решателях и нюансах задачи — в связанных статьях 📖.
🎯 Пост впервые опубликован John D. Cook.