Минисат, как найти все решения SAT эффективно

Question

Я нашел способ найти все решения, используя способ, описанный в этой ссылке.

Это работает нормально, но медленно. Поскольку он пересчитывает ограничения с самого начала, i_e не использует преимущества предыдущих вычислений.

Теперь, по этой ссылке, я увидел, что есть более эффективный способ найти все решения, использующие MiniSat в качестве библиотеки. Но путь там не описан.

Можете ли вы указать мне правильную документацию для эффективного поиска всех решений SAT?

Благодарю.

Answer 1

Более эффективный метод нахождения всех SAT-решений описан в статье Юла, Субраманяна, Цискаридзе и Малика "All-SAT с использованием минимальных блокирующих предложений".

Основная стратегия итеративного поиска решений и добавления блокирующих предложений одинакова, но блокирующие предложения генерируются с использованием новой идеи, которая уменьшает их размер. Созданные блокирующие предложения меньше, чем обычные наивные частичные назначения, и, следовательно, охватывают более удовлетворяющие назначения на одну итерацию, ускоряя процесс перечисления.

Насколько я знаю, не существует публичной реализации идей, содержащихся в этом документе, которые вы можете скачать и запустить.