Z3-solver throws 'model is not available‘在python 3上出现异常

Question

为了解决SAT问题，我决定使用微软和Python3的Z3-solver。目的是使用一个很长的模型(多达500,000个特征)并找到所有可能的解决方案。为了找到它们，我想将第一个解S1添加到初始方程中，并排除它，以此类推。我将使用while循环来完成此操作。解决SAT问题对我来说很重要，因为我想分析特征模型。

但是我遇到了一个问题，就是把某物加到初始方程式中。我将分享一个最小的例子：

# Import statements
import sys 
sys.path.insert(0,'/.../z3/bin')
from z3 import *        # https://github.com/Z3Prover/z3/wiki

def main():

    '''
    Solves after transformation a given boolean equation by using the Z3-Solver from Microsoft.
    '''

    fd = dict()
    fd['_r'] = Bool('_r')
    fd['_r_1'] = Bool('_r_1')

    equation = '''And(fd.get("_r"),Or(Not(fd.get("_r")),fd.get("_r_1")))'''

    # Solve the equation
    s = Solver()
    exec('s.add(' + equation + ')')
    s.check()
    print(s.model())

    ###################################
    # Successfull until here.
    ###################################

    s.add(Or(fd['_r'] != bool(s.model()[fd.get('_r')])))
    # s.add(Or(fd['_r'] != False))

    s.check()
    print(s.model())


if __name__=='__main__':
    main()

# Successfull...之后的第一个代码行抛出z3types.Z3Exception: model is not available错误。因此，我尝试了上面的代码行，将false简单地添加到模型中。这很好用。

我被困在这里了。我相信这个错误很容易解决，但我看不到解决方案。你们中有谁知道吗？谢谢!

Answer 1

只有在s.check()返回'sat‘之后，模型才可用。该模型将布尔命题映射为{True，False}，并通常将常量和函数映射为固定值。要求模型提供满足添加到求解器's‘中的公式的解释。在调用's.check()‘之前，我们不知道求解器状态是否可满足。

假设你想说：

s.add(Or(fd['_r'] != bool(s.model()[fd.get('_r')])))

这意味着在满足约束的模型中，应该具有这样的属性:如果模型下的'_r‘为真，则fd'_r’!= True；如果模型下的'_r‘为假，则fd'_r’!= False。这相当于说fd'_r‘!= '_r’。因此，在任何可能计算'_r‘的模型中访问'_r’的值并不是真正必要的，以便说明对它的评估。