代码之家 › 专栏 › 技术社区 › Pushpa

将Z3 QBF公式直接转换为pcnf

quantifiers z3py z3

Pushpa · 技术社区 · 7 年前

我正在使用Z3定理证明器(使用Z3Py:Python中的z3api)创建QBF(量化布尔公式)。

在Z3中有什么方法可以直接将qbf公式转换为 Prenex normal form ?

2 回复 | 直到 7 年前

alias 7 年前

我不认为有什么策略可以转换成Prenex,但你肯定可以应用量词消除策略,进一步处理你的公式。请注意,转换后的公式实际上看起来不像原始公式,因为它们是机械生成的。

举个例子:

from z3 import *

f = Function('f', IntSort(), IntSort(), IntSort())
x, y = Ints('x y')
p = ForAll(x, Or(x == 2, Exists(y, f (x, y) == 0)))

print Tactic('qe')(p)

在这里 qe 是量词消除策略。这将产生:

[[Not(Exists(x!0,
             Not(Or(x!0 == 2,
                    Exists(x!1,
                           And(f(x!0, x!1) <= 0,
                               f(x!0, x!1) >= 0))))))]]

有关战术的详细教程,请参阅: http://ericpony.github.io/z3py-tutorial/strategies-examples.htm

delcypher 7 年前

您可以使用skolemize策略(snf),根据定义,该策略将采用prenex形式。然而,它也会消除存在量词,这不是你想要的。这里有一个例子。

(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(declare-fun c (Int) Bool)
(assert
  (forall ((x Int))
    (or
      (exists ((y Int))
        (a y)
      )
      (exists ((z Int))
        (=>
          (b z)
          (c x)
        )
      )
    )
  )
)
(apply
  (and-then
  ; mode (symbol) NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full (default: skolem)
    (using-params snf :mode skolem)
  )
  :print_benchmark true
  :print false
)

当Z3给定上述值时,它将以如下方式响应

(declare-fun c (Int) Bool)
(declare-fun b (Int) Bool)
(declare-fun a (Int) Bool)
(assert (forall ((x Int))
          (or (exists ((y Int)) (a y)) (exists ((z Int)) (=> (b z) (c x))))))
(check-sat)

你可以通过跑步看到可用的战术

echo "(help-tactic)" | ./z3 -in | less

从bash shell。

不幸的是,我看不到有人说它会转换成prenex。