큰 정수 값을 가진 변수가 SMT의 성능에 영향을 줍니까?

Question

큰 정수 값이 SMT의 성능에 영향을 미치는지 궁금합니다. 때로는 큰 값으로 작업해야합니다. 주로 (즉, 다른 정수 항) 산술 연산 (주로 덧셈 및 곱셈)을 수행하고 결과 값을 제약 조건 (즉, 다른 정수 항)과 비교할 필요가 있습니다.

Answer 1

입력 문제에서 큰 정수 및/또는 이성은 경도의 최종 지표가 아닙니다. 입력에 작은 숫자 만 포함되어 있어도 Z3에서 내부적으로 많은 수를 생성 할 수 있습니다. Z3이 큰 유리수를 처리하는 데 많은 시간을 소비하는 많은 예를 보았습니다. 분자와 분모의 GCD를 계산하는 데 많은 시간이 소요됩니다. 각 GCD 계산에는 비교적 적은 시간이 걸리지 만 어려운 문제에서는 Z3이 수백만 개를 수행합니다. Z3은 순수한 정수 문제를 푸는 데 유리수를 사용합니다. 선형 산술을 해결하기 위해 Simplex 기반 알고리즘을 사용하기 때문입니다. 예를 게시하면보다 정확한 답을 줄 수 있습니다.