Может ли кто-нибудь указать на один или несколько веб-сайтов, где можно загрузить работающую реализацию решателя #SAT? Меня интересуют те, кто возвращает точное количество решений, а не приближение.
ds.algorithms
sat
software
Джорджо Камерани
источник
источник
Ответы:
Вы можете сделать это с SAT4J , просто перебирая все модели: http://www.sat4j.org/howto.php#models . Я полагаю, что большинство SAT решателей обладают этой способностью.
источник
Вы также можете попробовать #SAT solver "sharpSAT" ( веб-сайт , github ) для подсчета количества удовлетворительных заданий формул CNF.
источник
Одним из вариантов является использование библиотеки BDD, такой как JavaBDD . У всех таких библиотек либо есть функция, которая быстро считает решения, либо, по крайней мере, они облегчают написание такой функции. Недостаток, однако, заключается в том, что во многих случаях создание BDD будет медленным и может потребовать много памяти.
источник
Похожие темы: Лучший SAT Solver .
источник
Лучшее, что я нашел, это "c2d compiler". http://reasoning.cs.ucla.edu/c2d/
Он использует d-DNNF, и вам нужна опция -count .
источник
Обозреватель MBound, приведенный здесь http://www.cs.cornell.edu/~sabhar/, может дать подсчет моделей с вероятностными гарантиями. Это намного быстрее, чем перечислять все решения.
источник
Я написал небольшой модельный / простой имплицитный перечислитель . Это уже можно использовать для подсчета моделей с перечислением моделей, но это не очень практично. Если кому-то интересно, я могу расширить его, чтобы он считал модели из простых импликантов.
источник
Веб-сайт BeyondNP содержит хороший перечень существующих инструментов для решения #SAT (и других сложных проблем, связанных с формулами CNF). Вы также можете найти список инструментов для приблизительного подсчета моделей и компиляции знаний (задача преобразования CNF в, возможно, краткую структуру данных, которая часто поддерживает подсчет моделей за полиномиальное время).
Вы также можете найти список инструментов для предварительной обработки формул CNF, которые могут быть полезны для повышения производительности счетчиков моделей и различных эталонных тестов .
источник
Вот один из них называется tenorCSP и основан на инструменте под названием тензорные сети. Это объясняется в этой статье .
источник
Глюкоза - очень эффективный SAT-решатель, разработанный в университете Бордо.
https://www.labri.fr/perso/lsimon/glucose/
источник