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

[thesz]

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

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

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

Comments

[nivanych]

Правильный подход такой -
нужно для этих вещей строить некую теорию когомологий (скорее всего, каких-то пучков), а для когомологий строить теорию препятствий, которая позволит в немалом числе случаев отсекать ветви.
Всё это пока очень глубоко интуитивно, и не более.
Поэтому, прошу воспринимать, как шутку ;-)

[thesz]

Если я всё правильно понял, то так они и сделали. ;)

[nivanych]

Может быть, какие-то "такие" идеи там и присутствуют, но слово "когомологии" я там не увидел ;-)

[thesz]

Они строят деревья, как я понял, с отсечением. Практически твоя идея.

[anonim_legion]

Мне одному видится в заголовке поста отсылка к рассказу Станислава Лема?

[thesz]

Мне нравятся такие предложения, да. ;)