Предложение является выполнимым, если есть присвоение значений его переменным, которое делает его истинным; этот набор входных значений является решением проблемы.
Мы будем моделировать несколько задач, включая головоломки судоку, используя пропозициональную выполнимость, а затем решать их с помощью пакета SAT-решателя Pycosat на основе Python. Задачи SAT необходимо моделировать в конъюнктивной нормальной форме (CNF). Проблема в CNF, если это конъюнкция одного или нескольких предложений, где каждое предложение является дизъюнкцией литералов; просто, это И из ИЛИ.
Давайте рассмотрим простой пример.
Пусть p = (x₁ ∧ (¬x₁ ∨ x₂) ∧ x₃). Является ли p выполнимым?
Это предложение уже находится в конъюнктивной нормальной форме; в нем три дизъюнктивных предложения, соединенных союзами.
В Python предложение представлено в виде списка списков, где каждое дизъюнктивное предложение представлено в виде списка целых чисел. Знак соответствует логическому значению (+ для True и - для False), а абсолютное значение соответствует i-й переменной. Например, -1 соответствует x₁ = False, 2 соответствует x₂ = True и так далее.
Наша задача может быть записана для Python следующим образом:
>>> p = [[1], [-1, 2], [3]] >>> print(pycosat.solve(p)) [1, 2, 3]
Это решение означает: p выполнимо для x₁ = x₂ = x₃ = True.
Давайте посмотрим на другую проблему.
Дав список размера 4 с некоторыми значениями, найдите набор уникальных чисел от 1 до 4, чтобы каждое число встречалось в списке только один раз.
Пусть p(i, n) будет утверждением, которое истинно, когда число n находится в ячейке i.Поскольку у нас есть 4 ячейки, и каждая ячейка может иметь 4 возможных значения, мы имеем 16 различных переменных. Например, p(1, 2) = True означает, что ячейка 1 имеет значение 2.
def p(i, n): # returns variable number for a given cell / value combination return 4 * (i-1) + n
Мы можем смоделировать нашу проблему следующим образом:
- Для каждой ячейки с известным значением мы утверждаем p(i, n) = true.
sample_input = [0, 3, 0, 1]
clauses = []
for i in range(1, 5):
# lists in python are 0-indexed
digit = sample_input[i - 1]
if digit:
clauses.append([p(i, digit)])
print(clauses)
...
Out: [[7], [13]]
Этот вывод преобразуется в (x₇ ∧ x₁₃), где:
- x₇ ≡p(2, 3) значение ячейки 2 равно 3
- x₁₃ ≡p(4, 1) значение ячейки 4 равно 1.
2. Подтвердите, что список содержит все числа.
Мы будем строить это составное предложение постепенно. Построим предложение «q(n) = список содержит число n»:p(1, n) ∨ p(2 , n) ∨ p(3, n) ∨ p(4, n). Это можно упростить до q(n) = ∨⁴ᵢ₌₁p(i, n).
Теперь мы можем построить предложение «список содержит все числа»: q(1) ∧ q(2) ∧ q(3) ∧ q(4). Это можно упростить до ∧⁴ₙ₌₁∨⁴ᵢ₌₁p(i, n).
for n in range(1, 5):
# q(n) = list contains number n
q = []
for i in range(1, 5):
q.append(p(i, n))
clauses.append(q)
print(clauses)
...
[1, 5, 9, 13], [2, 6, 10, 14], [3, 7, 11, 15], [4, 8, 12, 16]
3. Утверждают, что ни одна ячейка не содержит более одного числа, используя конъюнкцию всех n, n` и i, где каждая переменная находится в диапазоне от 1 до 4 и n ≠ n` из
p(i, n) → ¬p(i, n`) ≡ ¬p(i, n) ∨ ¬p(i, n`)
for i in range(1, 5):
for n in range(1, 5):
for n_not in range(1, 5):
if n == n_not:
continue
clauses.append([-p(i, n), -p(i, n_not)])
print(clauses)
...
[-1, -2], [-1, -3], [-1, -4], [-2, -1], [-2, -3], [-2, -4], [-3, -1], [-3, -2], [-3, -4], [-4, -1], [-4, -2], [-4, -3], [-5, -6], [-5, -7], [-5, -8], [-6, -5], [-6, -7], [-6, -8], [-7, -5], [-7, -6], [-7, -8], [-8, -5], [-8, -6], [-8, -7], [-9, -10], [-9, -11], [-9, -12], [-10, -9], [-10, -11], [-10, -12], [-11, -9], [-11, -10], [-11, -12], [-12, -9], [-12, -10], [-12, -11], [-13, -14], [-13, -15], [-13, -16], [-14, -13], [-14, -15], [-14, -16], [-15, -13], [-15, -14], [-15, -16], [-16, -13], [-16, -14], [-16, -15]
Теперь мы можем решить задачу с помощью решателя SAT.
for sol in pycosat.itersolve(clauses): print(sol) ... [-1, -2, -3, 4, -5, -6, 7, -8, -9, 10, -11, -12, 13, -14, -15, -16] [-1, 2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, 13, -14, -15, -16]
Два решения:
- x₄ ∧ x₇ ∧ x₁₀ ∧ x₁₃ ≡ [4, 3, 2, 1]
- x₂ ∧ x₇ ∧ x₁₂ ∧ x₁₃ ≡ [2, 3, 4, 1]
Наконец, давайте смоделируем головоломку судоку как проблему выполнимости. Задача судоку очень похожа на предыдущую, поэтому мы не будем вдаваться в подробности некоторых утверждений.
Пусть p(i, j, n) — утверждение, истинное, когда число n находится в ячейке в i-й строке и j-м столбце. У нас есть 9 строк и 9 столбцов, и каждая ячейка может иметь 9 возможных значений; следовательно, у нас есть 729 различных переменных. Например, p(1, 2, 5) = True означает, что ячейка (1, 2) имеет значение 5.
def p(i, j, n): # return variable number for cell i,j with value n return 81 * (i-1) + 9 * (j-1) + n
Мы можем смоделировать нашу проблему следующим образом:
- Для каждой ячейки с известным значением мы утверждаем p(i, j, n) = true.
for i in range(1, 10):
for j in range(1, 10):
digit = puzzle[9 * (i-1) + j - 1]
if digit:
clauses.append([p(i, j, digit)])
2. Утверждают, что каждая строка содержит каждое число ∧⁹ᵢ₌₁∧⁹ₙ₌₁∨⁹ⱼ₌₁p(i, j, n).
for i in range(1, 10):
for n in range(1, 10):
q = []
for j in range(1, 10):
q.append(p(i, j, n))
clauses.append(q)
3. Утверждают, что каждый столбец содержит каждое число ∧⁹ⱼ₌₁∧⁹ₙ₌₁∨⁹ᵢ₌₁p(i, j, n).
for j in range(1, 10):
for n in range(1, 10):
q = []
for i in range(1, 10):
q.append(p(i, j, n))
clauses.append(q)
4. Утверждают, что каждый блок 3x3 содержит все числа ∧³ᵣ₌₀∧³ₛ₌₀∧⁹ₙ₌₁∨³ᵢ₌₁∨³ⱼ₌₁p(3r+i, 3s+j, n). Судоку состоит из девяти блоков 3x3. Переменные r и s позволяют нам перебирать каждый из этих девяти блоков. Затем мы используем i и j для перемещения внутри блока.
for r in range(3):
for s in range(3):
for n in range(1, 10):
q = []
for i in range(1, 4):
for j in range(1, 4):
q.append(p(3 * r + i, 3 * s + j, n))
clauses.append(q)
5. Утверждают, что ни одна ячейка не содержит более одного числа, путем конъюнкции всех n, n`, i и j, где каждая переменная находится в диапазоне от 1 до 9 и n ≠ n` из
p(i, i, n) → ¬p(i, j, n`) ≡ ¬p(i, j, n) ∨ ¬p(i, j, n`)
for i in range(1, 10):
for j in range(1, 10):
for n in range(1, 10):
for n_not in range(1, 10):
if n == n_not:
continue
clauses.append([-p(i, j, n), -p(i, j, n_not)])
Теперь мы можем решить задачу с помощью решателя SAT.
Код этой статьи можно найти здесь.
Обратите внимание, что эта статья представляет собой просто краткое изложение моего опыта изучения решателей SAT; Я никоим образом не являюсь экспертом в этой теме. Если вы найдете какие-либо ошибки, пожалуйста, дайте мне знать.
Логические уравнения для решателя судоку взяты из книги Розен К. Дискретная математика и ее приложения. 7-е изд.; 2011.
