Z3 마지막 유효 모델 가져 오기

Question

Z3 C++ API를 사용하여 일부 부울 변수 (b0, ..., bn)를 참이라고하는 만족스러운 수식을 찾습니다.

나는 부울 변수 b0, ..., bn을 포함하는 수식을 가지고 있으며 b0, ..., bn의 수가 최소 인 만족스러운 수식을 찾고 싶습니다.

처음에는 b0, ..., bn의 하위 집합을 찾아서 내 수식을 만족시킬 수 있습니다. 그리고 나는 점진적으로 더 작은 부분 집합을 찾습니다. 즉,이 부울 변수 중 하나가 거짓으로 뒤집 혔음).

더 작은 하위 집합을 찾을 수 없을 때 로컬 최소값을 찾았습니다. 즉, Z3에서 결과를 얻지 못했습니다. 이 시점에서 마지막 유효 모델에 액세스하려고합니다.

그럴 수 있습니까? "check"에 대한 호출이 불충분 할 때 Z3이 모델을 수정합니까? 그렇다면 어떻게 C++ API를 사용하여이 작업을 수행 할 수 있습니까? 솔버 반환 "앉아"당신은 모델을 검색 할 수 있습니다

Answer 1

사전에

많은 감사합니다. 모델은 해석자의 상태를 참조하므로 어설 션을 추가하면 상태가 변경되고 모델은 더 이상 유효성을 검사 할 때까지 유효하지 않으므로 sat를 반환합니다. 그래서 솔버가 SAT를 반환 할 때마다 모델을 검색 한 다음 마지막 모델을 제외하고 모두 방전 할 수 있습니다.

Answer 2

Nikolaj는 각 통화 후에 sat이되는 모델을 추적하고 설명 된 전략을 따르면 unsat을 얻을 때 마지막 모델을 반환해야합니다.

그러나 반복 된 호출을 모두 피할 수있는 또 다른 방법이있을 수 있습니다. 만족 문제 대신에, 최적화 문제로 문제를 던질 수 있습니다. 당신은 제어 변수 b0, b1, .. bn을 가지고 있다고 언급했는데 만족스러운 모델을 위해 그 숫자를 true으로 최소화하려고합니다. 이 변수의 수를 계산하는 메트릭을 만듭니다. 다음과 같이하십시오 :

metric = (if b0 then 1 else 0) 
     + (if b1 then 1 else 0) 
     + ... 
     + (if bn then 1 else 0) 

그런 다음 Z3의 최적화 루틴을 사용하여 metric을 최소화하십시오. 나는 이것이 당신이 한 통화에서만 찾고있는 해결책을 제공 할 것이라고 믿습니다.

유용한 참조 :

• 다음은 Z3 최적화 튜토리얼입니다 : http://rise4fun.com/z3opt/tutorialcontent/guide.

• 이 예에서는 특히 소프트 제약에 대해 이야기하고 있으며, 귀하의 경우에도 마찬가지로 적용 할 수 있습니다 : http://rise4fun.com/z3opt/tutorialcontent/guide#h25.

• 다음은 옵티 마이저에 대한 C++ API 참조입니다. http://z3prover.github.io/api/html/classz3_1_1optimize.html입니다.