Задача выполнимости булевых формул (SAT) 🧩 — определить, существует ли набор значений переменных, при котором все заданные логические выражения становятся истинными [1]. Если решение есть, следующая цель — перечислить все возможные варианты.
Возьмём знаменитую задачу о восьми ферзях ♟️ (или её обобщение для n ферзей). Её можно свести к SAT-проблеме, используя специальный решатель. Как?
Шаг 1️⃣: Представим шахматную доску 8×8 с переменными-индикаторами bᵢⱼ (от 1 до 8), где bᵢⱼ = true означает, что в клетке (i, j) стоит ферзь.
Требования:
1. В каждой строке ровно один ферзь.
– Минимум один: Для строки i создаём дизъюнкцию bᵢ₁ ∨ bᵢ₂ ∨ … ∨ bᵢ₈ ✅.
– Максимум один: Здесь сложность! Как запретить два ферзя в одной строке?
Подход 1️⃣: Используем импликации.
Например, для клетки (1,1):
b₁₁ ⇒ ¬(b₁₂ ∨ b₁₃ ∨ … ∨ b₁₈).
Преобразуем в клаузу: ¬b₁₁ ∨ ¬b₁₂ ∨ ¬b₁₃ ∨ … ∨ ¬b₁₈ ⚠️.
Подход 2️⃣: Парные запреты.
Для всех пар клеток в строке добавляем условие: ¬bᵢₖ ∨ ¬bᵢₗ (например, ¬b₁₁ ∨ ¬b₁₂, ¬b₁₁ ∨ ¬b₁₃ и т.д.). Всего 28 комбинаций для одной строки 🔄.
Плюс: Формула сразу получается в конъюнктивной нормальной форме (КНФ) — AND из OR-условий 🎯.
Аналогичные правила применяем для столбцов и диагоналей. Вуаля! Остаётся передать формулу SAT-решателю.
Интересное:
🔗 [Уроки работы с решателем Z3](https://example.com)
🔗 [Специальные решения для задачи о ферзях](https://example.com)
[1] Если формул несколько, их можно объединить через AND в одну.
💡 Пост впервые опубликован в блоге John D. Cook. 📚