Z3에서 외부 SAT 솔버 호출

Question

내가 근무하는 회사에서 여러 SAT 솔버에 액세스 할 수 있습니다. 각 SAT 솔버가 Z3 SMT 솔버의 성능에 어떤 영향을 주는지 분석하고 싶습니다.

Z3에서 외부 SAT 솔버를 호출 할 수 있습니까? 그렇지 않은 경우 외부 솔버를 호출하도록 Z3을 수정해야합니까?

Answer 1

Z3은 긴밀하게 통합 된 내부 SAT 솔버를 사용하기 때문에 이것은 쉬운 작업이 아닐 것이라고 생각합니다. SAT 솔버와의 긴밀한 통합은 Z3가 외부 SAT 솔버의 로우 레벨 API를 통해 상호 작용해야한다는 것을 의미합니다. 푸시 및 팝 기능. 이러한 API는 표준화되지 않았으므로 예를 들어 MiniSat의 경우는 예를 들어 Lingeling과 통합하는 작업. Z3은 모듈화 된 아키텍처가 확장되어 있기 때문에 가능하지 않다고 말하지는 않지만 이것이 중요한 작업이 될 것이라고 생각합니다.

Z3 개발자 중 한 명이 나타나서 나를 잘못 알았을 수도 있습니다.