Z3 中的部分赋值

Question

我有一个布尔公式（格式：CNF），我使用 Z3 SAT 求解器检查其可满足性。当公式可满足时，我有兴趣获得部分分配。我在 OR 门的简单公式上尝试了 model.partial=true，但没有得到任何部分赋值。

你能建议如何做到这一点吗？除了它是部分的之外，我对分配没有任何限制。

Answer 1

Z3的部分模型模式只针对函数模型。对于命题公式，不能保证模型使用最少数量的赋值。相反，SAT 求解器的默认模式是找到完整的作业。

假设您对最小数量的文字感兴趣，这样文字的连词就暗示了公式。您可以使用 unsat cores 来获取此类子集。这个想法是，您首先找到公式 F 的模型作为文字 l1、l2、...、ln 的合取。然后鉴于这是 F 的模型，我们有 l1 & l2 & ... & ln & not F 是不可满足的。所以想法是断言 "not F" 并检查 "not F" 模假设 l1, l2, .., ln 的可满足性。由于结果是不饱和的，您可以查询 Z3 以检索 l1、l2、..、ln 中的不饱和核心。

从 python 你要做的是创建两个求解器对象：

    s1 = Solver()
    s2 = Solver()

然后你分别加上F, Not(F):

    s1.add(F)
    s2.add(Not(F))

然后您使用两个求解器找到 F 的简化模型：

    is_Sat = s1.check()
    if is_Sat != sat:
       # do something else, return
    m = s1.model()
    literals = [sign(m, m[idx]()) for idx in range(len(m)) ]
    is_sat = s2.check(literals)
    if is_Sat != unsat:
       # should not happen
    core = s2.unsat_core()
    print core

哪里

    def sign(m, c):
        val = m.eval(c)
        if is_true(val):
           return c
        else if is_false(val):
           return Not(c)
        else:
           # should not happen for propositional variables.
           return BoolVal(True)

当然还有其他方法可以减少文字集。一种部分廉价的方法是急切地评估每个子句并从模型中添加文字，直到模型中的至少一个文字满足每个子句为止。换句话说，您正在寻找最小的击球集。你必须在 Z3 之外实现它。

Z3 中的部分赋值

partial assignments in Z3

z3

sat