如何让 Z3 返回最小模型? [英] How do I get Z3 to return minimal model?

问题描述

如果我给 Z3 一个像 p 这样的公式 |q，我希望 Z3 返回 p=true, q=don't care (或者 p 和 q 切换)，但它似乎坚持为 p 和 q 赋值(即使我没有完成在调用 Eval() 时打开).除了对此感到惊讶之外，我的问题是如果 p 和 q 不是简单的道具会怎样.vars 但是很昂贵的表达式，我知道通常 p 或 q 都会为真.有没有一种简单的方法可以让 Z3 返回一个最小"模型而不是浪费时间试图同时满足 p 和 q?我已经尝试过 MkITE 但这没什么区别.还是我必须使用某种策略来强制执行此操作?

If I give Z3 a formula like p | q, I would expect Z3 to return p=true, q=don't care (or with p and q switched) but instead it seems to insist on assigning values to both p and q (even though I don't have completion turned on when calling Eval()). Besides being surprised at this, my question then is what if p and q are not simple prop. vars but expensive expressions and I know that typically either p or q will be true. Is there an easy way to ask Z3 to return a "minimal" model and not waste its time trying to satisfy both p and q? I already tried MkITE but that makes no difference. Or do i have to use some kind of tactic to enforce this?

谢谢！附注.我想补充一点，我已经关闭了 AUTO_CONFIG，但 Z3 正在尝试将值分配给 or 的两个分支中的常量:例如，在下面的代码片段中，我希望它分配给 path2_2 和 path2_1 或 path2R_2 和 path2R_1，但不能同时分配给两者

thanks! PS. I wanted to add that I have turned off AUTO_CONFIG, yet Z3 is trying to assign values to constants in both branches of the or: eg in the snippet below I want it to assign either to path2_2 and path2_1 or to path2R_2 and path2R_1 but not both

   (or (and (select a!5 path2_2) a!6 (select a!5 path2_1) a!7)
       (and (select a!5 path2R_2) a!8 (select a!5 path2R_1) a!9))

推荐答案

Z3 具有称为相关性传播的功能.本文中对此进行了描述.它做你想做的.请注意，在大多数情况下，相关性传播会对性能产生负面影响.在我们的实验中，它只对包含量词的问题有用(量词推理是如此昂贵以至于它是有回报的).默认情况下，Z3 将在包含量词的问题中使用相关性传播.否则，它不会使用它.这是一个关于如何在问题没有量词时将其打开的示例(该示例也可在线获得此处)

Z3 has a feature called relevancy propagation. It is described in this article. It does what you want. Note that, in most cases relevancy propagation has a negative impact on performance. In our experiments, it is only useful for problems containing quantifiers (quantifier reasoning is so expensive that it is pays off). By default, Z3 will use relevancy propagation in problems that contain quantifiers. Otherwise, it will not use it. Here is an example on how to turn it on when the problem does not have quantifiers (the example is also available online here)

x, y = Bools('x y')
s = Solver()
s.set(auto_config=False, relevancy=2)
s.add(Or(x, y))
print s.check()
print s.model()

这篇关于如何让 Z3 返回最小模型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！