有没有办法使用 SMTLIB2 语法检索所有令人满意的分配？
我使用的求解器是 Z3 和 CVC4。
问问题
103 次
1 回答
0
虽然在“纯”SMTLIB2 中没有办法做到这一点，即只使用单个文件并且没有外部输入，但如果您有一个可以与求解器交互的应用程序，那么有一个标准技巧可以做到这一点。您在交互模式下运行求解器，您可以一次向其发送一个 SMTLIB2 命令，然后通过以下方式与其交互（伪代码）：
def get_all_assignments(instance):
create solver in interactive mode
for each declaration, assertion, etc. in instance:
send assertion to solver
let response := None
while response is not UNSAT:
send command '(check-sat)' to solver and get response
if response is SAT:
send command '(get-model)' to solver and get model
print model
send the solver a new assertion which is the negation of the model
实际上，每次找到令人满意的分配时，您都会向模型添加一个新约束，以防止求解器再次找到该分配，并要求它重新求解。当求解器返回 UNSAT 时，您就知道您已经找到了每一个令人满意的任务。
有关此主题和 Z3 实现的进一步阅读，请参阅Z3：找到所有令人满意的模型和Z3py：检查方程的所有解决方案。
于 2015-11-18T22:36:27.947 回答