Z3에서 귀납적 사실 증명

Question

저는 Microsoft의 SMT 솔버 인 Z3에서 귀납적 사실을 입증하려고합니다. Z3은 일반적으로 Z3 guide (8 단원 : 데이터 유형)에 설명 된대로이 기능을 제공하지 않지만 사실을 입증하려는 도메인을 제한 할 때 가능하다고 생각합니다. 다음의 예를 생각해

(declare-fun p (Int) Bool) 
(assert (p 0)) 

(assert (forall ((x Int)) 
    (=> 
    (and (> x 0) (<= x 20)) 
    (= (p (- x 1)) (p x))))) 
(assert (not (p 20))) 

(check-sat) 

솔버는 (p 20)이 유효 함을 의미한다 unsat 제대로 응답합니다. 문제는 더 이상이 제약 조건을 완화하면 (앞의 예에서 20을 20보다 큰 임의의 정수로 대체 함) 해결자가 unknown으로 응답합니다.

원본 문제를 해결하기 위해 Z3을 길게 취하지 않기 때문에이 이상한 점을 발견하지만, 상한선을 하나 늘리면 갑자기 불가능 해집니다. 나는 다음과 같이 정량에 패턴을 추가하는 시도 : 잘 작동하는 것 같다,하지만 지금은 상한은 40입니다

(declare-fun p (Int) Bool) 
(assert (p 0)) 

(assert (forall ((x Int)) 
    (! (=> 
    (and (> x 0) (<= x 40)) 
    (= (p (- x 1)) (p x))) :pattern ((<= x 40))))) 
(assert (not (p 40))) 

(check-sat) 

이 내가 더 나은 같은 사실을 증명하기 위해 Z3를 사용할 수 없다는 뜻, 또는 내 문제를 잘못 공식화하고 있습니까?

Answer 1

Z3은 한정사 인스턴스화를 제어하기 위해 많은 경험적 방법을 사용합니다. 그 중 하나는 "인스턴스화 깊이"를 기반으로합니다. Z3은 모든 표현식에 "깊이"속성을 붙입니다. 모든 사용자 제공 어설 션에는 깊이 0 태그가 지정됩니다. 한정 기호가 인스턴스화되면 새 표현식의 깊이가 부딪칩니다. Z3은 사전 정의 된 임계 값보다 큰 깊이로 태그가 지정된 표현식을 사용하여 한정 기호를 인스턴스화하지 않습니다. 문제에서, 임계 값에 도달 : (p 40) 깊이 0, (p 39) 깊이 1, (p 38) 깊이 2,

, 당신은 옵션을 사용해야하는 임계 값을 늘리려면 등 : 다음은

(set-option :qi-eager-threshold 100) 

을 이 옵션이있는 예제는 http://rise4fun.com/Z3/ZdxO입니다.

물론이 설정을 사용하면 Z3의 시간이 초과됩니다 (예 : (p 110)).

미래에 Z3은 "한계 수량화"를 더 잘 지원할 것입니다. 대부분의 경우, 이런 종류의 한정 기호를 처리하는 최선의 방법은 그것을 확장하는 것입니다. 프로그래밍 방식의 API를 사용하면 식을 Z3으로 보내기 전에 식을 "인스턴스화"할 수 있습니다.

p = Function('p', IntSort(), BoolSort()) 

s = Solver() 

s.add(p(0)) 
s.add([ p(x+1) == p(x) for x in range(40)]) 
s.add(Not(p(40))) 

print s.check() 

마지막으로, Z3에서, 산술 기호를 포함하는 패턴은 매우 효과적이지 못하다 : 여기 파이썬 (http://rise4fun.com/Z3Py/44lE)의 일례이다. 문제는 Z3이 해결하기 전에 수식을 전처리한다는 것입니다. 그러면 산술 기호가 포함 된 대부분의 패턴은 절대로 일치하지 않습니다. 패턴/트리거를 효과적으로 사용하는 방법에 대한 자세한 내용은 this article을 참조하십시오. 작성자는 slide deck도 제공합니다.