Z3 파이썬으로 양자 제거 사용하기

g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0)))을 만족하는 A, B, C, D의 값을 찾으려고합니다. solve(g)을 사용합니다. 여기에는 많은 가능한 해결책이 있는데, 하나는 A=1,B=-1,C=D=0이지만 Z3은 이것을 수행 할 수 없습니다 (solve(g)은 종료되지 않습니다).Z3 파이썬으로 양자 제거 사용하기

Z3이 비선형 (그러나 간단한) 공식을 할 수 있습니까? 아마도 QE 전략이나 이와 관련하여 어떤 것을 지정할 수 있습니까?

출처

2013-02-19 Vu Nguyen

Z3은 한정 기호 제거 기술을 가지고 있습니다. 우리는 사용 솔버를 작성하여이를 사용할 수 있습니다 :

s = Then('qe', 'smt').solver()

이 명령은 처음 정량 제거를 적용 한 후 SMT 해결사를 호출하는 해결사를 생성합니다. 그러나 Z3에는 비선형 수식의 한정 기호 제거에 대한 지원이 매우 제한적입니다. 귀하의 예는 A * i + B * j + C * k + D <= 0을 포함하고 있기 때문에 비선형 적입니다. 따라서 qe 전술은 한정 기호를 제거 할 수 없습니다.

비선형 산술을 위해 더 나은 QE 지원을 구현할 수 있다면 좋을 것입니다.

출처

2013-02-19 02:08:07

감사합니다. Leonardo, 비선형 arith에 대한 QE가 지원되지 않는다면, 왜 이런 종류의 수식을 볼 때'solve (g)'가 알려지지 않거나 지원되지 않을까요? 대신, 뭔가를하려고하는 것처럼 보입니까? 또한 Z3은 비선형 * 등식 * 또는 다른 비선형 산술 클래스에 대해 QE를 지원합니까? 다른 SMT 솔버가 Non linear arith에 대한 지원을 제공하는지 알고 있습니까? 다시 한 번 감사드립니다 –

Z3은 경험적 인스턴스화와 모델 기반 수량화 인스턴스를 사용합니다. 이러한 방법은 완전하지는 않지만 많은 문제를 해결할 수 있습니다. Z3에 보내지는 대부분의 문제 (수량 한정 기호 포함)는 결정할 수없는 부분이지만 Z3이 그 일부를 푸는 것을 방해하지는 않습니다. –

제가 아는 한, Z3은 비선형 산술을 가장 잘 지원합니다. (한정자없는) 비선형 산술 문제에 매우 효과적입니다. 이 기사 끝 부분의 비교를 참조하십시오. http://research.microsoft.com/en-us/um/people/leonardo/files/IJCAR2012.pdf –

Z3 파이썬으로 양자 제거 사용하기

답변

관련 문제