Определенно есть способ использовать описанный вами решатель SAT для поиска всех решений проблемы SAT, хотя, возможно, это не самый эффективный способ.
Просто используйте решатель, чтобы найти решение вашей исходной проблемы, добавьте предложение, которое ничего не делает, кроме исключения только что найденного вами решения, используйте решатель, чтобы найти решение новой проблемы, и так далее. Продолжайте, пока не столкнетесь с проблемой, которую невозможно решить.
Например, предположим, что вы хотите удовлетворить (X or Y) and (X or Z). Есть пять решений:
Четыре с X истинным, 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 ищет решение, он много узнает о проблеме, но не возвращает вам всю эту информацию - он просто дает вам решение, которое он нашел. Когда вы снова запустите решатель, он должен заново изучить всю информацию, которая была выброшена.
person
Community
schedule
03.09.2012
