Про sentential decision diagrams
https://www.youtube.com/watch?v=_5Estmve91o - видео.
http://reasoning.cs.ucla.edu/sdd/ - основная страничка.
https://github.com/hahaXD/sdd - исходный код библиотеки. С основной страницы тоже можно скачать, но надо совершать какие-то дополнительные действия. На Rust, если кому интересно.
Я про них писал. И, вроде бы, не совсем наврал, несмотря на то, что писал не разобравшись до конца. Я и сейчас не совсем всё понимаю. ;)
Вот интересная статья про преобразование CNF в SDD с помощью чего-то-типа-CDCL. Результаты на 7-ой странице и они довольно интересны: если SDD в целом менее объёмны, чем ROBDD, то хорошо построенная SDD будет в 2..100 раз меньше ROBDD. "Хорошо построенная" это либо "снизу вверх", либо "сверху вниз с постобработкой".
http://reasoning.cs.ucla.edu/sdd/ - основная страничка.
https://github.com/hahaXD/sdd - исходный код библиотеки. С основной страницы тоже можно скачать, но надо совершать какие-то дополнительные действия. На Rust, если кому интересно.
Я про них писал. И, вроде бы, не совсем наврал, несмотря на то, что писал не разобравшись до конца. Я и сейчас не совсем всё понимаю. ;)
Вот интересная статья про преобразование CNF в SDD с помощью чего-то-типа-CDCL. Результаты на 7-ой странице и они довольно интересны: если SDD в целом менее объёмны, чем ROBDD, то хорошо построенная SDD будет в 2..100 раз меньше ROBDD. "Хорошо построенная" это либо "снизу вверх", либо "сверху вниз с постобработкой".