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 是不可满足的。 所以这个想法是断言“非 F”并检查“非 F”模假设 l1、l2、..、ln 的可满足性。由于结果是 unsat，您可以查询 Z3 以检索 l1、l2、..、ln 之间的 unsat 核心。

你要做的是从 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 之外实现它。