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

[thesz]

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

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

Minisat ещё и не самый свежий.