z3 中最大满足子集查找器的文档示例中的错误

Question

我正在尝试使用 z3 文档示例中的代码来查找 z3 中最令人满意的子集。这是我复制的代码：

from z3 import *

def main():
    x, y = Reals('x y')
    soft_constraints = [x > 2, x < 1, x < 0, Or(x + y > 0, y < 0), Or(y >= 0, x >= 0), Or(y < 0, x < 0), Or(y > 0, x < 0)]
    hard_constraints = BoolVal(True)
    solver = MSSSolver(hard_constraints, soft_constraints)
    for lits in enumerate_sets(solver):
        print("%s" % lits)


def enumerate_sets(solver):
    while True:
        if sat == solver.s.check():
           MSS = solver.grow()
           yield MSS
        else:
           break

class MSSSolver:
   s = Solver()
   varcache = {}
   idcache = {}

   def __init__(self, hard, soft):
       self.n = len(soft)
       self.soft = soft
       self.s.add(hard)       
       self.soft_vars = set([self.c_var(i) for i in range(self.n)])
       self.orig_soft_vars = set([self.c_var(i) for i in range(self.n)])
       self.s.add([(self.c_var(i) == soft[i]) for i in range(self.n)])

   def c_var(self, i):
       if i not in self.varcache:
          v = Bool(str(self.soft[abs(i)]))
          self.idcache[v] = abs(i)
          if i >= 0:
             self.varcache[i] = v
          else:
             self.varcache[i] = Not(v)
       return self.varcache[i]

   # Retrieve the latest model
   # Add formulas that are true in the model to 
   # the current mss

   def update_unknown(self):
       self.model = self.s.model()
       new_unknown = set([])
       for x in self.unknown:
           if is_true(self.model[x]):
              self.mss.append(x)
           else:
              new_unknown.add(x)
       self.unknown = new_unknown
      
   # Create a name, propositional atom,
   #  for formula 'fml' and return the name.

   def add_def(self, fml):
       name = Bool("%s" % fml)
       self.s.add(name == fml)
       return name

   # replace Fs := f0, f1, f2, .. by
   # Or(f1, f0), Or(f2, And(f1, f0)), Or(f3, And(f2, And(f1, f0))), ...

   def relax_core(self, Fs):
       assert(Fs <= self.soft_vars)
       prefix = BoolVal(True)
       self.soft_vars -= Fs
       Fs = [ f for f in Fs ]
       for i in range(len(Fs)-1):
           prefix = self.add_def(And(Fs[i], prefix))
           self.soft_vars.add(self.add_def(Or(prefix, Fs[i+1])))

   # Resolve literals from the core that 
   # are 'explained', e.g., implied by 
   # other literals.

   def resolve_core(self, core):
       new_core = set([])
       for x in core:
           if x in self.mcs_explain:
              new_core |= self.mcs_explain[x]
           else:
              new_core.add(x)
       return new_core


   # Given a current satisfiable state
   # Extract an MSS, and ensure that currently 
   # encountered cores are avoided in next iterations
   # by weakening the set of literals that are
   # examined in next iterations.
   # Strengthen the solver state by enforcing that
   # an element from the MCS is encountered.

   def grow(self):
       self.mss = []
       self.mcs = []
       self.nmcs = []
       self.mcs_explain = {}
       self.unknown = self.soft_vars
       self.update_unknown()
       cores = []
       while len(self.unknown) > 0:
           x = self.unknown.pop()
           is_sat = self.s.check(self.mss + [x] + self.nmcs)
           if is_sat == sat:
              self.mss.append(x)
              self.update_unknown()
           elif is_sat == unsat:
              core = self.s.unsat_core()
              core = self.resolve_core(core)
              self.mcs_explain[Not(x)] = {y for y in core if not eq(x,y)}
              self.mcs.append(x)
              self.nmcs.append(Not(x)) 
              cores += [core]              
           else:
              print("solver returned %s" % is_sat)
              exit()
       mss = [x for x in self.orig_soft_vars if is_true(self.model[x])]
       mcs = [x for x in self.orig_soft_vars if not is_true(self.model[x])]
       self.s.add(Or(mcs))
       core_literals = set([])
       cores.sort(key=lambda element: len(element))
       for core in cores:
           if len(core & core_literals) == 0:
              self.relax_core(core)
              core_literals |= core
       return mss

main

函数的输出看起来不错，但是我对如下布尔问题感兴趣：

p, q = z3.Bools('p q')

hard = z3.Not(q)
soft = [z3.Not(p), z3.Not(q), p]

solver = MSSSolver(hard, soft)     
mms = tuple(enumerate_sets(solver))

print(mms[0][0].sexpr())

这会打印出

'|Not(q)|'

，表明

Not

未被解释，而不是解释为 z3 表达式。我不太明白这段代码的内部原理，所以我发现很难调试它。尽管如此，在

str

中使用

c_var

似乎很奇怪 - 这可能是问题所在吗？

Answer 1

我不确定您为什么认为

|Not(q)|

意味着

Not

未解释。事实并非如此。像这样的

main

：

def main():
    p, q = Bools('p q')
    hard = Not(q)
    soft = [z3.Not(p), z3.Not(q), p]
    solver = MSSSolver(hard, soft)
    for lits in enumerate_sets(solver):
        print("%s" % lits)

输出为：

[Not(q), p]
[Not(p), Not(q)]

这对我来说非常有意义。两条线都满足

Not(q)

，您将其称为硬约束。它们的区别在于，一个具有

p

，另一个具有

Not(p)

，这些都属于您的软约束。这正是最大满足子集的集合。