Z3 실제 산술 및 통계

Question

는 Z3 /smt2 /st가 실수 엔진 "/ 문제가 많은 일을한다"경우 판단하기 위해 도움이 될 수 생산하는 통계의 Z3의 실수를 사용하여 인코딩 된 문제를 감안할 때? 내 경우

, 나는 문제의 두 대부분 해당 인코딩이 모두 실수를 사용. 그러나 인코딩의 "작은"차이는 런타임에서 큰 차이를 만듭니다. 즉, 인코딩 A는 2 : 30 분, 인코딩 B는 13 분입니다. Z3 통계는 conflicts 및 quant-instantiations은 대부분 동일하지만, 다른 예를 grobner, pivots 및 nonlinear-horner를 들어 아니라는 것을 보여줍니다.

두 개의 서로 다른 통계는 gist으로 사용할 수 있습니다.

편집 (레오의 코멘트를 해결하기 위해) :

두 버전에 의해 생성 된 SMT2 인코딩입니다 ~ 30K 라인과 실수가 사용되는 주장은 모든 코드 뿌려있다. 가장 큰 차이점은 인코딩 B가 0.0에서 1.0 범위의 덜 구체화 된 실수 형 상수를 사용한다는 것입니다.이 상수는 부등식으로 묶입니다. 0.0 < r1 < 1.0 또는 0.0 < r3 < 0.75 - r1 - r2 인 반면, 인코딩에서 이러한 많은 지정되지 않은 상수가 동일한 범위의 고정 된 실수 값, 예를 들어 0.1 또는 0.75 - 0.01으로 대체되었습니다. 두 인코딩 모두 비선형 실수 산술을 사용합니다. r1 * (1.0 - r2). 두 인코딩에서

몇 가지 임의의 예는 gist으로 사용할 수 있습니다. 발생하는 모든 변수는 위에 설명 된대로 구체화되지 않은 실제 값입니다.

PS : 예를 들어,

(define-sort $Perms() Real) 
(declare-const $Perms.$Full $Perms) 
(declare-const $Perms.$None $Perms) 
(assert (= $Perms.Zero 0.0)) 
(assert (= $Perms.Write 1.0)) 

상당한 성능 저하를 입힐 고정 실제 값에 대한 별칭을 도입 하는가?

Answer 1

새로운 비선형 산술 해석은 산술만을 포함하는 문제에서만 사용됩니다. 문제는 한정 기호를 사용하기 때문에 새로운 비선형 해석은 사용되지 않습니다. 따라서 Z3은 Simplex (피벗 통계), Groebner Basis (groebner 통계) 및 Interval Propagation (horner stat)의 조합을 기반으로 한 이전 방식을 사용합니다. 이것은 완전한 방법은 아닙니다. 또한, gist에 게시 한 프래그먼트를 기반으로 Groebner 기반은 그리 효과적이지 않습니다. 이 방법은 대개 동등성이 많은 문제에 효과적입니다. 아마도 오버 헤드 일뿐입니다. 당신은 옵션 NL_ARITH_GB=false를 사용하여 비활성화 할 수 있습니다. 물론 이것은 게시 한 문제의 단편을 기반으로 한 추측에 불과합니다. 부호화 및 AB 사이

차이는 상당하다. 인코딩 A은 근본적으로 선형 문제입니다. 몇 가지 상수가 실수 값으로 고정 되었기 때문입니다. Z3은 선형 산술 문제에 대해 항상 완벽했습니다. 따라서 성능 차이를 설명해야합니다.

별명에 대한 질문에 대해서는, 별칭을 소개하는 선호하는 방법은 다음과 같습니다

는

(define-const $Perms.$Zero $Perms 0.0) 
(define-const $Perms.$Write $Perms 1.0) 

Z3는 선형 방정식을 사용하여 변수를 제거하는 전처리를 포함한다. 이 사전 처리기는 한정 기호가 포함 된 문제에서 기본적으로 비활성화되어 있습니다.이 설계 결정은 한정자에서 트리거/패턴을 광범위하게 사용하는 프로그램 검증 도구에 의해 동기 부여됩니다. 변수 제거 프로세스는 신중하게 설계된 트리거/패턴을 수정하고 총 런타임에 영향을 줄 수 있습니다. Z3에서 새로운 전술/전략 프레임 워크를 사용하여이 전처리 기가 적용되도록 할 수 있습니다. 당신은 simplifier을 실행 한 후 방정식을 해결 (및 제거 변수를) 다음 기본 솔버 엔진을 smt 실행 Z3 말하고있다

(check-sat-using (then simplify solve-eqs smt)) 

이 전략으로 명령

(check-sat) 

을 대체 할 수 있습니다. 전술 및 전략에 대한 자세한 내용은 tutorial에서 확인할 수 있습니다.