SAT-солверы — это программы, решающие задачу выполнимости булевых формул (SAT), которая является NP-полной. Это означает, что любые NP-полные задачи, такие как задача коммивояжера, раскраска графа или Судоку, могут быть сведены к SAT и решены с помощью этих инструментов. SAT-солверы находят значения переменных, при которых булева формула становится истинной, предоставляя эффективный способ решения сложных задач, которые иначе требовали бы экспоненциального времени.

На примере Судоку автор демонстрирует, как преобразовать правила игры в систему булевых ограничений. Для каждой клетки (i,j) и цифры k вводится переменная x_{i,j,k}, где true означает, что клетка содержит цифру k. Правила игры переводятся в ограничения: каждая клетка должна содержать ровно одну цифку (x_{i,j,1} ∨ x_{i,j,2} ∨ ... ∨ x_{i,j,9} и ¬x_{i,j,k} ∨ ¬x_{i,j,l} для k≠l), каждая цифра должна встречаться ровно один раз в строке, столбце и под-сетке. SAT-солвер находит удовлетворяющее всем этим ограничениям присвоение значений переменным, решая головоломку.

• SAT и MILP-солверы недооценены: первые хорошо знакомы инженерам, вторые — нет, хотя MILP позволяет естественно выразить оптимизацию и ограничения.
• Исторически открытые MILP-солверы отставали от коммерческих, что сдерживало их использование.
• SAT-солверы и MILP-солверы дополняют друг друга: SAT хорошо для задач «есть/нет», MILP — для задач оптимизации.
• Практически любую задачу можно выразить как MILP, и SAT-солверы могут быть использованы для решения MILP.

Простое введение в z3

Изучение мира решателей ограничений на простых примерах.

Что такое решатели?

Решатели — это инструменты, которые принимают правила и ограничения, а затем находят решение. Они не всегда быстрее специальных алгоритмов, но гораздо гибче при изменении условий. Применяются для планирования, распределения ресурсов и других задач.

Терминология

В документации z3 много жаргона. Например, «Sort» означает тип, а «constants» — это переменные, которыми оперирует решатель. Solver работает со своим языком SMT-LIB2, а библиотеки переводят код в этот язык.

Простое уравнение

Решим уравнение x + 4 = 7. Вот код на Rust:

use z3::{Solver, ast::Int};
fn main() {
    let solver = Solver::new();
    let x = Int::new_const("x");
    solver.assert(&(x + 4).eq(&7));
    assert_eq!(solver.check(), SatResult::Sat);
    let model = solver.get_model().unwrap();
    println!("x = {}", model.eval(&x, true).unwrap());
}

Решатель находит x = 3. Это базовый пример, но он показывает принцип работы.

• Обсуждение причин некорректных ответов в задаче о сдаче (coin change) при использовании решателя Z3 без нижних границ, что приводит к минимизации до отрицательной бесконечности.
• Рекомендации ресурсов для изучения SAT/SMT-решателей, включая конкретные PDF-документы и статьи.
• Обсуждение практического применения решателей (Z3, OR-Tools, MiniZinc) для различных задач, включая игры и оптимизацию запросов.
• Сравнение и рекомендации по выбору решателей для начинающих на Python, с упоминанием Z3, OR-Tools и CPMpy.
• Трудности моделирования проблем для решателей и важность правильной постановки ограничений для избежания неинтуитивного поведения.
• Обсуждение технических особенностей интеграции решателей в языки программирования, таких как перегрузка операторов в Rust.
• Упоминание о применении решателей для доказательства теорем и поиска контрпримеров, например, к гипотезе Гольдбаха.