z3 - Z3 bool 変数の算術演算

Question

aiZ3 には、SAT 問題を定式化するためにbj、 、 、 などのブール変数がたくさんあります。ckただし、私の問題では、考慮すべき 3 つの算術制約があります。

a1 + a2 + a3 + ... + an = 1
b1 + b2 + b3 + ... + bn = 0
c1 + c2 + c3 + ... + cn <= 1

Z3 API を使用して、変数の型を変更せずにこれら 3 つの算術制約を定式化するにはどうすればよいでしょうか (つまり、デフォルトではすべてブール型)。

Answer 1

ブール値を if 式に埋め込むことができます。たとえば、次のように記述できます。

  if(a1,1,0) + if(a2,1,2) + ...

やや特別な目的の機能として、この時点で C、.NET、および Java API から組み込みカーディナリティ演算子を使用してカーディナリティ制約を直接入力することもできますが、python や Ocaml ではできません。また、lia2pb タクティックは、(上記のように) if-then-else 式を使用するゴールを変換し、それらを疑似ブール制約に変換します。