列表中的项目，在z3模型中部分评估

Question

考虑下面的例子：

from z3 import *

data1 = [BitVec("x_{}".format(i), 8) for i in range(10)]
data2 = [BitVec("x_{}".format(i), 8) for i in range(20)]
var = BitVec("var", 16)

s = Solver()
s.add(Not(Or(
    And(var == 100, Sum(data1) == 10),
    And(var == 200, Sum(data2) == 10))))

while True:
    s.push()
    if s.check() == sat:
        if len(s.model()) != 11 and len(s.model()) != 21:
            print(len(s.model()))
            print(s.model())
            break
    s.pop()

产生以下结果：

12
[x_2 = 252,
 x_9 = 248,
 x_1 = 255,
 x_3 = 96,
 x_5 = 192,
 x_4 = 223,
 x_17 = 0,
 var = 0,
 x_0 = 0,
 x_6 = 252,
 x_7 = 254,
 x_8 = 248]

结果似乎是正确的，但我不明白为什么x_17出现在列表中

另一个结果是：

1
[var = 0]

空列表是否被认为是Sum(data1) == 10的有效解决方案？ 它如何明确指定列表必须包含10或20个项目？ 但我的主要问题是：为什么要提出部分清单作为解决方案

在这个例子中：

from z3 import *
data = [BitVec("x_{}".format(i), 8) for i in range(10)]
s = Solver()
s.add(Sum(data1) == 10)
while True:
    s.push()
    if s.check() == sat:
        if len(s.model()) != 10:
            print(len(s.model()))
            print(s.model())
            break
    s.pop()

该计划并不是从循环中产生的，没有用部分列表提出解决方案。 也许And操作员的设计具有类似短路的行为

Answer 1

第一个节目

您的约束条件是：

s.add(Not(Or(
    And(var == 100, Sum(data1) == 10),
    And(var == 200, Sum(data2) == 10))))

通过De Morgan's laws，这相当于：

s.add(Or(var != 100, Sum(data1) != 10))
s.add(Or(var != 200, Sum(data2) != 10))

考虑如果求解器集^ {CD1>}为^ {< CD2>}：两个析取都是真的，因此系统是可满足的。因此，不管所有的x设置为什么，也不管总和是什么

总而言之，任何var不是100的赋值和200都是问题的模型。请注意，z3只会分配“足够”的变量，使问题处于sat状态，因此您看不到其他变量。（但如果您确实需要它们，则可以获取它们的值；z3只是告诉您，它们并不重要，因为不将它们放入模型中。）

第二程序

在第二个问题中（将data1重命名为data之后），进入无限循环的是Python程序。Z3实际上几乎立即回答您的查询，但您的if条件是：

if len(s.model()) != 10:

由{}发现的模型中正好有10个东西。所以你一直在z3外循环。也许你想让那if行读== 10