在 z3 中编码伪布尔约束的最有效方法是什么? [英] What is the most efficient way to encode pseudoboolean constraints in z3?

问题描述

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

I think there's two different relevant cases here:

案例 1:

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

I have a set of boolean variables and I want another boolean variable which is true if any of these variables are true. I'm currently doing this by making the boolean variables integers which are then set using expressions of the form:

(ite (boolean_expr) 1 0)

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

I then set the overall boolean just using a sum and a greater than

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

案例 2(这可能不是真正的伪布尔值):

Case 2 (this may not really be pseudoboolean):

我有两组布尔变量:

set1 = n_1,n_2....

set2 = m_1,m_2....

我想添加一个约束，说明 set1 中设置为 true 的变量数等于 set2 中设置为 true 的变量数.

I'd like to add a constraint that says the number of variables set to true in set1 is equal to the number set to true in set2.

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

As above, I'm currently doing this by using integers instead of booleans and setting each one with an ite of the form:

n_1 = (ite (boolean_expr) 1 0)

然后说:

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

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

In each case, is using integer variables the most efficient way to do it, or is there a better way?

谢谢.

推荐答案

您目前可以使用整数来编码 PB 约束.您必须将变量限制在区间 0, 1 内.例如:

You can currently use integers to encode PB constraints. You have to bound the variables to be in the interval 0, 1. For example:

 (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 为您进行重写

If you set the logic to QF_LIA, then Z3 will automatically try to re-encode these constraints using bit-vectors. In the verbose output you will see that Z3 invokes a tactic pb2bv that does the rewriting for you

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)

这篇关于在 z3 中编码伪布尔约束的最有效方法是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！