저는 Z3를 처음 접했고 오픈 소스 프로그램의 경우 z3 솔버를 사용하여 효율성을 높이고 싶습니다.
약 1000 개 이상의 값이 있습니다.
(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(declare-const a4 Int)
...
그 결과
(declare-const x1 Int)
(declare-const x2 Int)
...
(assert (= (+ a1 a2) x1) // in reality its not "plus" but more sophisticated
(assert (= (+ a3 a4) x2) // however for simplicity lets keep it at that here.
...
이제 모든 x1 ~ x500 + 변수의 값이 서로 다르고 중복이 없는지 확인하고 싶습니다.
물론 할 수 있습니다
(assert (not (= x1 x2)))
(assert (not (= x1 x3)))
(assert (not (= x1 x4)))
...
(assert (not (= x2 x3)))
(assert (not (= x2 x4)))
...
(assert (not (= x718 719)))
그리고 그것은 작동 할 것입니다. 그러나 더 나은 해결책이 있습니까?
감사합니다!
다음을 사용할 수 있습니다 distinct(이 예 참조 ).
(assert (distinct x1 ... x500))
AFAIK, 이것은 일반적으로 예제에서 제시 한 것과 마찬가지로 일련의 부등식으로 내부적으로 확장됩니다.
토론 : 다음은이 인코딩의 효율성에 대한 순전히 이론적 인 토론입니다. z3매우 효율적인 SMT 솔버이므로 단순히 도구를 실행하는 것보다 더 복잡한 것을 시도 할 필요가 없습니다.
평등의 부정 (예 :) (not (= x y))은 일반적으로 한 쌍의 부등식으로 나뉩니다.
x < y \/ x > y
의 말을하자 x < y및 x > y이름이 변경 B1과 B2다음 절을 SAT 엔진에 공급되는 각각 :
B1 \/ B2
이제 문제가 주어지면 수백 개의 절이 있습니다. 이들은 모두 선형 산술 수준에서 서로 관련되지만 SAT 엔진이 작동하는 부울 수준에서는 관련이 없습니다. 따라서 SAT 엔진은 일반적으로 <연산자 의 전이 속성을 위반하는 (상당한) 수의 불일치 부분 진실 할당을 생성 할 가능성이 있습니다.
x < y /\ y < z /\ z < x
이러한 충돌은 LRA에 대한 이론 솔버가 조기 정리 호출 중에 드러내고 잘못된 할당을 차단하는 충돌 절을 학습하여 부울 수준에서 해결됩니다.
시도 할 수있는 작업 :
문제가 그러한 단순화를 인정 한다면 (이름 x1 ... x500이 완전히 임의적 인 것으로 간주 될 수 있다면 나중에 뒤섞을 수 있습니다.) 변수에 대해 엄격한 총 순서를 부과하는 더 나은 결과를 얻을 수 있습니다 x1 ... x500. 예를 들어
x1 < x2 /\ x2 < x3 /\ ... /\ x499 < x500
사용 가능한 옵션 인 경우를 사용 하여 조기 정리 호출 의 빈도를 높일 z3수 있습니다 (참고 : z3이러한 호출을 얼마나 자주 수행 하는지 잘 모르겠습니다 ).
편집하다:
변수에 할당 할 수있는 값 집합 x_i이 유한하고 크기가 다소 제한되어있는 경우 카디널리티 제약을 정의하기 위해 x_i비표준 z3확장을 사용하여 특정 값을 가진 변수의 수를 계산할 수 있습니다.
(assert
((_ at-most 1)
(= x1 0)
(= x2 0)
...
(= x500 0)
)
)
...
% repeat for all possible values
...
이 변경이 성능에 미치는 영향에 대해 잘 모르겠습니다. 정상적인 상황에서는 이전에 충돌하는 할당을 나타내므로 성능에 긍정적 인 영향을 미칩니다 (예 : [1] 참조 ). 그러나 상당히 많은 수의 변수와 변수에 대한 후보 값의 큰 도메인을 다루고 x_i있으므로 부울 수준에서 검색을 평탄화하는 것은 과잉 일 수 있습니다.
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다