...необычный решатель задач булевской выполнимости.

Забавные подробности воспоследуют.

http://www.cs.bgu.ac.il/~mcodish/Papers/Sources/lopstr07.pdf

SAT был использован для проверки завершимости набора правил переписывания. Кодирование проблемы в CNF и запуск Minisat быстрее в сотни раз, чем специализированное решение.

Minisat ещё и не самый

Поскольку у меня последнее время идиосинкразия к большим постам, буду конспективно ( Read more... )

Вершиной переборных алгоритмов я считаю решение проблемы выполнимости булевой формулы.

Ибо переборный алгоритм по сути своей доказательство теоремы.

Вот здесь находится краткое описание, как работают современные системы ( Read more... )

В гугле.

Предыдущие серииНапомню кратенько содержание ( Read more... )

( на таблицах решений, само собой, NP-полное, но всё же! )