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 )

但是对于两组，我看不到它是如何完成的。

感谢您的关注。

4

1 回答 1

3

您在消息中描述的操作(contains S1 S2)是子集关系。如果我们将整数集编码为从 Int 到 Boolean 的函数（例如 in: max value in set z3），那么S1和S2被声明为：

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

然后，我们可以说这S1是S2通过断言

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

我们只是说 in 中的任何元素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为真，当且仅当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 回答