0

为了解决 SAT 问题，我决定使用 Microsoft 的 Z3-solver 和 Python 3。目的是采用长模型（最多 500,000 个特征）并找到所有可能的解决方案。为了找到它们，我想将第一个解 S1 添加到初始方程并排除 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到模型中。这工作得很好。

我被困在这里。我相信这个错误很容易解决，但我没有看到解决方案。你们中的一个吗？谢谢！

4

1 回答 1

2

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

假设你想说：

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

意味着在满足约束的模型中应该具有这样的性质，如果模型下'_r'为真，则fd['_r']！=真，如果模型下'_r'为假，则fd[' _r'] != 错误。这相当于说 fd['_r'] != '_r'。因此，实际上没有必要在任何可能评估“_r”的模型中访问“_r”的值来说明对它的评估。

于 2016-09-15T02:04:50.573 回答