时间戳

首页 > 解决方案 > 在 Z3Py 中编码允许集

python - 在 Z3Py 中编码允许集

问题描述

基于论证框架理论，我正在尝试使用 Z3Py 证明者对可接受集进行编码。但是，我遇到了一些问题，并希望获得有关如何改进它的任何指示。

根据Wikipedia的定义，当且仅当一组参数E是无冲突的并且其所有参数对于E都是可接受的时，它才是可接受的。

基于以下带参数的有向图：a, b, c, d, e 和关系：(a, d), (a, b), (b, c), (c, b), (c, d) , (e, a) 可容许集的正确解是：[], [e], [c], [c, e], [b, e], [b, d, e]

我开始使用 Z3Py，但在编码时遇到了问题。

到目前为止，我有这个：

from z3 import *

a, b, c, d, e = Bools('a b c d e')
arguments = [a, b, c, d, e]
solver = Solver()
relations = [(a, d), (a, b), (b, c), (c, b), (c, d), (e, a)]

# ensure there are no conflicting arguments
for relation in relations:
    solver.append(Implies(relation[0], Not(relation[1])))

for argument in arguments:
    # if not attacked then removed any arguments attacked by this argument
    if len([item for item in relations if item[1] == argument]) == 0:
        solver.append([Not(attacked[1]) for attacked in relations if attacked[0] == argument])

    # if self attacking remove the argument
    if len([item for item in relations if item[1] == argument and item[0] == argument]) > 0:
        solver.append(Not(argument))

    # get all attackers
    attackers = [item[0] for item in relations if item[1] == argument]
    for attacker in attackers:
        # get defenders of the initial argument (arguments attacking the attacker)
        defenders = [item[0] for item in relations if item[1] == attacker]
        defending_z3 = []
        if len(defenders) > 0:
            for defender in defenders:
                if defender not in attackers:
                    defending_z3.append(defender)
            if len(defending_z3) > 0:
                solver.append(Implies(Or([defend for defend in defending_z3]), argument))
        else:
            solver.append(Not(argument))

# get solutions
solutions = []
while solver.check() == sat:
    model = solver.model()
    block = []
    solution = []
    for var in arguments:
        v = model.eval(var, model_completion=True)
        block.append(var != v)
        if is_true(v):
            solution.append(var)
    solver.add(Or(block))
    solutions.append(solution)

for solution in solutions:
    print(solution)

执行时，它给了我以下解决方案：[]，[c]，[d]，[b，d]，[b，d，e]，其中只有 3 个是正确的：

  1. [b, d] 不正确，因为 d 不能自卫（e 是 d 的防御者）
  2. [d] 再次不正确，因为 d 无法为自己辩护
  3. [e] 缺失
  4. [c, e] 缺失
  5. [b, e] 缺失

任何帮助，将不胜感激。

标签： pythonpython-3.xsetz3pysat

解决方案

这对于 SMT 求解来说是一个非常好的问题，z3 将能够相对轻松地处理这些问题，即使您有非常大的集合。

您的编码想法是正确的，但是您将相等性混为一谈：在测试变量是否与另一个变量相同时应该小心。为此，请使用 Python 的eq方法。（如果你使用==，那么你会得到一个符号相等测试，这不是你在这里寻找的。）

鉴于此，我倾向于将您的问题编码如下：

from z3 import *

a, b, c, d, e = Bools('a b c d e')
arguments = [a, b, c, d, e]
solver = Solver()
relations = [(a, d), (a, b), (b, c), (c, b), (c, d), (e, a)]

# No conflicting arguments
for relation in relations:
    solver.add(Not(And(relation[0], relation[1])))

# For each element, if it is attacked, then another element that
# attacks the attacker must be present:
for argument in arguments:
    # Find the attackers for this argument:
    attackers = [relation[0] for relation in relations if argument.eq(relation[1])]

    # We must defend against each attacker:
    for attacker in attackers:
        defenders = [relation[0] for relation in relations if relation[1].eq(attacker)]

        # One of the defenders must be included:
        solver.add(Implies(argument, Or(defenders)))

# Collect the solutions:
while solver.check() == sat:
    model = solver.model()
    block = []
    solution = []

    for var in arguments:
        v = model.eval(var, model_completion=True)
        block.append(var != v)
        if is_true(v):
            solution.append(str(var))

    solver.add(Or(block))
    solution.sort()
    print(solution)

希望代码应该易于理解。如果没有，请随时提出具体问题。

当我运行它时，我得到：

[]
['c']
['c', 'e']
['e']
['b', 'e']
['b', 'd', 'e']

这似乎与您预测的解决方案相匹配。

推荐阅读