https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.190/Mitarbeiter/balint/SAT2012.pdf

Решил освежить.

Вот цитата:
Scaling behavior with N: The survey propagation algorithm scales linearly with N on formulas generated ( Read more... )

https://www.cs.cmu.edu/~mheule/publications/bcd.pdfRead more... )

https://en.wikipedia.org/wiki/2-satisfiabilityRead more... )

В статье про разложение на заблокированные ограничения (РЗО) упоминается забавный приём под названием SAT sweeping - переведём его, как "чистку схемы" (ЧС ( Read more... )

Предыдущая версия.

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

Однако.

Для каждого выводимого литерала нам надо вычислять два набора ограничений: с выводимым литералом и разрешение (resolution) по выводимому литералу.

Сейчас у меня получается, что количество множеств ограничений будет пропорционально 2количество выводимых литералов. Даже если ( Read more... )

Предыдущие серии тут и по ссылкам оттуда ( Read more... )

https://cca.informatik.uni-freiburg.de/papers/BalyoFrohlichHeuleBiere-SAT14.pdf и ещё статья про blocked clause decomposition https://www.cs.cmu.edu/~mheule/ ( Read more... )

Полуторагодичной давности: https://thesz.livejournal.com/1536050.htmlRead more... )

https://arxiv.org/pdf/cond-mat/0408190.pdfRead more... )

вот тут https://www-cs-faculty.stanford.edu/~knuth/programs.html есть ссылка на программу, что позволяет решать проблемы Игры Жизнь через представление их в виде проблемы логической выполнимости.

И по мелочам там интересное. ;)