将Z3 QBF公式直接转化为pcnf

Question

我正在使用 Z3 定理证明器（使用 Z3Py：Python 中的 Z3 API）来创建 QBF（量化布尔公式）。

Z3有没有办法直接把你的qbf公式转换成Prenex normal form？

Answer 1

我不认为有转换为 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

Answer 2

您可以使用 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 的产品。

将Z3 QBF公式直接转化为pcnf

Converting Z3 QBF formula directly to pcnf

quantifiers

z3

z3py