съдържа за два комплекта в Z3

Ако искам да проверя дали едно множество има елементи от друго множество също е възможно?

Например (съдържа Set1 Set2):

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

Множествата са крайни. И максималната стойност на наборите е пет, а минималната е 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 )

Но за два комплекта не виждам как става.

Благодаря за вниманието.


z3
person Robert    schedule 14.03.2013    source източник

Отговори (1)


arrow_upward
3
arrow_downward

Операцията (contains S1 S2), която описвате в съобщението си, е релацията на подмножеството. Ако кодираме набори от цели числа като функции от Int към Boolean (както в: макс. стойност в набор z3), тогава 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))))))

Ако минималните стойности на наборите, които кодирате, са известни във "времето на кодиране" (и са малки). Можем да използваме още едно кодиране, базирано на Bit-вектори. В това кодиране наборът е битов вектор. Ако наборите съдържат само стойности между 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)))
person Leonardo de Moura    schedule 14.03.2013
comment
Не искам подмножество, защото мога да имам contains [1,2] [3,4,2] -> is true. - person Robert; 15.03.2013
comment
Актуализирах отговора с израз, който може да се използва за проверка дали два набора имат общ елемент или не. По същество просто се проверява дали кръстовището е празно или не. - person Leonardo de Moura; 15.03.2013