Можно ли использовать SAT-решение для поиска всех решений?

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

Предположим, что у меня есть SAT-решатель, который, учитывая булеву формулу в конъюнктивной нормальной форме, возвращает либо решение (присваивание переменной, которое удовлетворяет формуле), либо информация, что проблема является неудовлетворительной.

Могу ли я использовать этот решатель для поиска всех решений?

Ответ 1

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

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

Например, предположим, что вы хотите удовлетворить (X or Y) and (X or Z). Существует пять решений:

Четыре с X true, Y и Z произвольные.
Один с X false, Y и Z true.

Итак, вы запускаете свой решатель, и пусть он дает вам решение (X, Y, Z) = (T, F, F). Вы можете исключить это решение --- и только это решение --- с ограничением

not (X and (not Y) and (not Z))

Это ограничение можно переписать в качестве предложения

(not X) or Y or Z

Итак, теперь вы можете запустить свой решатель по новой проблеме

(X or Y) and (X or Z) and ((not X) or Y or Z)

и т.д.

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

Ответ 2

Конечно, это возможно. Когда MiniSat [1] находит решение

s SATISFIABLE
v 1 2 -3 0

(решение 1 = True, 2 = True, 3 = False), тогда вы должны поместить в исходное предложение CNF [2], запрещающее это решение:

-1 -2 3 0

(что означает, что 1 или 2 должно быть False или 3 должно быть True). Затем вы снова решаете. Вы делаете это до тех пор, пока решатель не вернет UNSAT, то есть больше не будет решений проблемы. Вы вставляете одно предложение для каждой итерации, и каждое предложение будет иметь тот же формат, что и решение, за исключением того, что оно все инвертировано и имеет 0 в конце

Это намного быстрее, если использовать интерфейс С++ для MiniSat, так как он может сохранять промежуточные данные, и итерации будут быстрее.

[1] http://minisat.se/

[2] http://fairmut3x.wordpress.com/2011/07/29/cnf-conjunctive-normal-form-dimacs-format-explained/