在 z3 中编码伪布尔约束的最有效方法是什么？答案

【问题标题】：What is the most efficient way to encode pseudoboolean constraints in z3?在 z3 中编码伪布尔约束的最有效方法是什么？
【发布时间】：2013-11-26 19:43:18
【问题描述】：

我认为这里有两个不同的相关案例：

案例一：

我有一组布尔变量，我想要另一个布尔变量，如果其中任何一个变量为真，则该变量为真。我目前正在通过将布尔变量设为整数来实现这一点，然后使用以下形式的表达式进行设置：

(ite (boolean_expr) 1 0)

然后我只使用总和和大于来设置整体布尔值

(> (+ b1 b2 b3...) 0)

案例 2（这可能不是真正的伪布尔值）：

我有两组布尔变量：

set1 = n_1,n_2....

set2 = m_1,m_2....

我想添加一个约束，表示在 set1 中设置为 true 的变量数等于在 set2 中设置为 true 的数量。

如上所述，我目前通过使用整数而不是布尔值来执行此操作，并使用以下形式的 ite 设置每个整数：

n_1 = (ite (boolean_expr) 1 0)

然后说：

n_1+n_2+.... = m_1+m_2......

在每种情况下，使用整数变量是最有效的方法，还是有更好的方法？

谢谢。

【问题讨论】：

标签： z3

【解决方案1】：

您目前可以使用整数来编码 PB 约束。您必须将变量绑定在区间 0、1 内。例如：

 (set-logic QF_LIA)
 (declare-const n1 Int)
 (declare-const n2 Int)
 (assert (<= 0 n1))
 (assert (<= n1 1))
 (assert (<= 0 n2))
 (assert (<= n2 1))
 (assert (>= (+ n1 n2) 1))
 (check-sat)

如果你将逻辑设置为 QF_LIA，那么 Z3 会自动尝试重新编码这些约束使用位向量。在详细输出中，您将看到 Z3 调用了一个策略 pb2bv 来为您进行重写

z3 ty.smt2 /v:10
(simplifier :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(propagate-values :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(ctx-simplify :num-steps 17)
(ctx-simplify :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(simplifier :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(solve_eqs :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(elim-uncnstr-vars :num-exprs 10 :num-asts 171 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(simplifier :num-exprs 10 :num-asts 173 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(pb2bv :num-exprs 4 :num-asts 180 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(simplifier :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(propagate-values :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(solve_eqs :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(max-bv-sharing :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(bit-blaster :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(aig :num-exprs 3 :num-asts 178 :time 0.00 :before-memory 0.77 :after-memory 0.77)
(ast-table :capacity 640 :size 178)
(sat-status
  :inconsistent    false
   :vars            2
  :elim-vars       0
  :lits            2
  :assigned        0
  :binary-clauses  1
  :ternary-clauses 0
  :clauses         0
  :del-clause      0
  :avg-clause-size 2.00
  :memory          0.77)

【讨论】：

【解决方案2】：

z3 在某些时候添加了原生伪布尔约束

def AtMost(args)
def AtLeast(args)
def PbLe(args, k)
def PbGe(args, k)
def PbEq(args, k, ctx=None)

(Python Docs)

SMTLib2：

(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
; 9 = 1a + 2b + 4c + 8d
(assert ((_ pbeq 9 1 2 4 8) a b c d))
(check-sat)
(get-model) ; 0 1 0 1
(exit)

【讨论】：