3

私はsatソルバーのコンテキストでこの質問をしています。x1, x2, x3 ... x100の間にランダムに値が割り当てられた100個の整数変数があるとします1 to N。x1 to x100の少なくとも1つの変数がからの値のそれぞれを持っていることを確認したいと思います1 to N。

ここで、この問題をsatソルバー制約でエンコードしたいと思います。制約を書いている間、私は値を知らないので、N以下のようにコーディングするのは難しいです-

(assert (x1 = 0 or x2 = 0 or ... x100 = 0))
(assert (x1 = 1 or x2 = 1 or ... x100 = 1))
(assert (x1 = 2 or x2 = 2 or ... x100 = 2))
...
(assert (x1 = N or x2 = N or ... x100 = N))

最後に、Nの値を2と主張すると、上記の制約は機能しなくなります。さらに、パフォーマンス上の理由から、配列や解釈されていない関数は使用したくありません。

アップデート ：

要するに、制約は次のとおりです-

  1. N <100
  2. （N = 20としましょう）、20個の変数があり、それらはx_1からx_100までのいずれかである可能性があります。したがって、この制約により、1からNまでの値ごとに少なくとも1つの変数が割り当てられるようになります。
  3. 残りの変数（100-N）の値は互いに重複する可能性があります。

誰かが私にいくつかの提案をすることができますか？

4

3 に答える 3

2

distinct述語を使用します。参照：http ：//smtlib.cs.uiowa.edu/theories/Core.smt2

于 2012-09-25T18:18:14.970 に答える
2

最大n個のx_i変数（ランダムに選択）について、カイルの答えを個別の変数と組み合わせてみませんか？

これにより、次のようなモデルが得られます（N =50および100x_i変数の場合）。

 x = [0 -> 1,
  1 -> 11,
  2 -> 50,
  3 -> 1,
  4 -> 2,
  5 -> 1,
  6 -> 36,
  7 -> 1,
  8 -> 34,
  9 -> 1,
  10 -> 13,
  11 -> 5,
  12 -> 7,
  13 -> 23,
  14 -> 1,
  15 -> 40,
  16 -> 42,
  17 -> 1,
  18 -> 1,
  19 -> 1,
  20 -> 16,
  21 -> 33,
  22 -> 1,
  23 -> 17,
  24 -> 20,
  25 -> 1,
  26 -> 9,
  27 -> 44,
  28 -> 1,
  29 -> 49,
  30 -> 26,
  31 -> 1,
  32 -> 29,
  33 -> 46,
  34 -> 8,
  35 -> 1,
  36 -> 27,
  37 -> 1,
  38 -> 1,
  39 -> 32,
  40 -> 1,
  41 -> 31,
  42 -> 1,
  43 -> 1,
  44 -> 14,
  45 -> 1,
  46 -> 1,
  47 -> 1,
  48 -> 1,
  49 -> 1,
  50 -> 35,
  51 -> 19,
  52 -> 43,
  53 -> 22,
  54 -> 1,
  55 -> 1,
  56 -> 1,
  57 -> 1,
  58 -> 21,
  59 -> 1,
  60 -> 1,
  61 -> 39,
  62 -> 28,
  63 -> 12,
  64 -> 1,
  65 -> 1,
  66 -> 1,
  67 -> 1,
  68 -> 1,
  69 -> 41,
  70 -> 1,
  71 -> 25,
  72 -> 1,
  73 -> 6,
  74 -> 1,
  75 -> 1,
  76 -> 1,
  77 -> 1,
  78 -> 1,
  79 -> 24,
  80 -> 1,
  81 -> 30,
  82 -> 38,
  83 -> 3,
  84 -> 4,
  85 -> 1,
  86 -> 1,
  87 -> 1,
  88 -> 1,
  89 -> 1,
  90 -> 18,
  91 -> 1,
  92 -> 47,
  93 -> 37,
  94 -> 1,
  95 -> 45,
  96 -> 1,
  97 -> 15,
  98 -> 48,
  99 -> 10,
  else -> 1],

これを実現するZ3Pyスクリプトは、ランダムなものではなく、最初のN個のインデックスを制約できると仮定しています（定数の代わりにxの関数を使用しているため、記述が高速です）： http: //rise4fun.com/Z3Py/M3TG

次は、ランダムなインデックスのセットに対してこれを実行するためのコードですが、インポートを使用できないため、Z3Py @ Riseでこれを実行することはできません。したがって、ローカルで実行する必要があります。

from random import *
from z3 import *

x = Function('x', IntSort(), IntSort())

M = 100
N = 50

s = Solver()
idxs = sample(xrange(M),N) # get N random ids from sequence {1,...M}
print idxs

distinctlist = []
for i in range(M):
  s.add(And(x(i) >= 1, x(i) <= N))
  if i in idxs:
    distinctlist.append(x(i))

print distinctlist

s.add(Distinct(distinctlist))

print "checking..."

r = s.check()
print r
if r == sat:
  print s.model()

（このクエリを不飽和にすると、タイムアウトになる可能性があることに注意してください。）

于 2012-09-27T15:11:30.823 に答える
1

私は書くだろう

(assert (or (and (> x1 0) (<= x1 n))
            (and (> x2 0) (<= x2 n))
            ...same for x3 thru x99...
            (and (> x100 0) (<= x100 n))))

nこれは、0以上である限り、後でどの値がアサートされても機能します。

于 2012-09-27T06:24:18.100 に答える