0

セットに別のセットの要素があるかどうかを確認したい場合も可能ですか？

例（Set1 Set2を含む）：

contains [1,2] [3,5] -> is false
contains [1] [2,3, 1] -> is true

セットは有限です。また、セットの最大値は5で、最小値は0です。セットの値は、5より大きく0より小さくすることはできません。

例えば：

[1,5,3] -> valid set
[1,8,2] -> invalid set

セットのみの場合、セットに値が存在するかどうかを確認するのは簡単でした。それは次のようでした：

( declare-sort Set 0 )

( declare-fun contains (Set Int) bool )

( declare-const set Set )

( declare-const A Int )

( assert ( contains set A ))
( assert ( not (contains set 0 )))
( check-sat )

しかし、2つのセットについては、それがどのように行われるかわかりません。

ご清聴ありがとうございました。

4

1 に答える 1

3

メッセージで説明する操作(contains S1 S2)はサブセット関係です。整数のセットをIntからブール値までの関数としてエンコードする場合（たとえば、setz3のmaxvalue）、S1およびS2は次のように宣言されます。

(declare-fun S1 (Int) Bool)
(declare-fun S2 (Int) Bool)

次に、それは主張することによってS1のサブセットであると言うことができますS2

(assert (forall ((x Int)) (=> (S1 x) (S2 x))))

S1の要素はすべての要素でもあると言っていますS2。

編集

式を使用して(exists ((x Int)) (and (S1 x) (S2 x)))、セットS1とS2要素が共通しているかどうかを確認できます

編集終了

セットの最小要素は、セットz3の最大値で行ったようにエンコードできます。たとえば、の最小要素がであるS1としmin_S1ます。

; Now, let min_S1 be the min value in S1
(declare-const min_S1 Int)
; Then, we now that min_S1 is an element of S1, that is
(assert (S1 min_S1))
; All elements in S1 are bigger than or equal to min_S1
(assert (forall ((x Int)) (=> (S1 x) (not (<= x (- min_S1 1))))))

エンコードしているセットの最小値が「エンコード時」にわかっている場合（そして小さい場合）。ビットベクトルに基づくさらに別のエンコーディングを使用できます。このエンコーディングでは、セットはビットベクトルです。セットに0〜5の値しか含まれていない場合は、サイズ6のビットベクトルを使用できます。アイデアは、ビットiがtrueの場合i、セットの要素である場合に限ります。

主な操作の例を次に示します。

(declare-const S1 (_ BitVec 6))
(declare-const S2 (_ BitVec 6))
(declare-const S3 (_ BitVec 6))

; set equality is just bit-vector equality
(assert (= S1 S2))

; set intersection, union, and complement are encoded using bit-wise operations

; S3 is  S1 union S2
(assert (= S3 (bvor S1 S2))) 

; S3 is S1 intersection of S2  
(assert (= S3 (bvand S1 S2)))

; S3 is the complement of S1   
(assert (= S3 (bvnot S1))) 

; S1 is a subset of S2 if  S1 = (S1 intersection S2), that is
(assert (= S1 (bvand S1 S2)))

; S1 is the empty set if it is the 0 bit-vector
(assert (= S1 #b000000))

; To build a set that contains only i we can use the left shift
; Here, we assume that i is also a bit-vector
(declare-const i (_ BitVec 6))
; S1 is the set that contains only i
; We are also assuming that i is a value in [0, 5]
(assert (= S1 (bvshl #b000001 i)))
于 2013-03-14T17:39:12.213 に答える