는 Z3

Question

와 모델을 생성 할 수 없습니다

나는 내가 smt2 형식으로 믿는다 "knapsack.smt2"라는 파일의 배낭 문제에 대한 다음 예제 코드를하고 난 Z3의 최신 버전이 있습니다

을 그러나

(declare-const s1 Int) 
(declare-const o1 Int) 
(declare-const b1 Bool) 

(declare-const s2 Int) 
(declare-const o2 Int) 
(declare-const b2 Bool) 

(declare-const s3 Int) 
(declare-const o3 Int) 
(declare-const b3 Bool) 


(declare-const sack-size Int) 
(declare-const filled Int) 

(assert (< o1 sack-size)) 
(assert (< o2 sack-size)) 
(assert (< o3 sack-size)) 

(assert (>= o1 0)) 
(assert (>= o2 0)) 
(assert (>= o3 0)) 

(assert (=> (not b1)(= o1 o2))) 
(assert (=> (not b2)(= o2 o3))) 

(assert (=> b1 (= (+ o1 s1) o2))) 
(assert (=> b2 (= (+ o2 s2) o3))) 
(assert (=> b3 (= (+ o3 s3) filled))) 

(assert (=> (not b3) (= o3 filled))) 
(assert (<= filled sack-size)) 

(assert (= o1 0)) 


(assert (= s1 3)) 
(assert (= s2 4)) 
(assert (= s3 5)) 
(assert (= sack-size 20)) 

(assert (= filled 13)) 

(check-sat) 
(get-model) 

, 내가 실행 "Z3 -m knapsack.smt2"나는 다음과 같은 오류 메시지가 :

라인 (46)은 마지막 줄에 "(수-모델)"입니다

>> z3 -m knapsack.smt2 
unsat 
(error "line 46 column 10: model is not available") 

.

아무도 왜 이것이 작동하지 않는지 말할 수 있습니까?

감사합니다.

Answer 1

Z3은 만족스러운 인스턴스에 대한 모델을 생성합니다. 수식이 만족스럽지 않습니다. 제약

(assert (= o1 0)) 
(assert (= s1 3)) 
(assert (= s2 4)) 
(assert (= s3 5)) 
(assert (= filled 13)) 

우리가

를 사용 o1 = 0 및 s1 = 3, s2 = 3, s3 = 5 및 filled = 13, 하는 제약

(assert (=> (not b1)(= o1 o2))) 
(assert (=> b1 (= (+ o1 s1) o2))) 

우리가 사용 o2 = 0 또는 o2 = 3 그. 우리는 o3 = o2 또는 o3 = o2 + 3 이

(assert (=> b3 (= (+ o3 s3) filled))) 
(assert (=> (not b3) (= o3 filled))) 

를 사용하여 우리는 o3 = 8 또는 o3 = 13 이제

, 우리는 충돌을 볼 수 있다고이

(assert (=> (not b2)(= o2 o3))) 
(assert (=> b2 (= (+ o2 s2) o3))) 

를 사용

o2 = 0 or o2 = 3 
o3 = 8 or o3 = 13 
o3 = o2 or o3 = o2 + 3 

012 우리가 o2 = 0을하려고하면 3,516,

우리는 우리가 o2 = 3을하려고하면 시켰음 공식

o3 = 8 or o3 = 13 
o3 = 0 or o3 = 3 

우리는 시켰음 공식을 얻을 수

o3 = 8 or o3 = 13 
o3 = 3 or o3 = 6