정확히 수량 한정 기호는 SMT가 완성 되었습니까?

Question

저는 다양한 SMT 솔버, 주로 Z3, CVC4 및 VeriT를 살펴 보았습니다. 그들은 수량 한정자로 SMT 문제를 풀 수있는 능력에 대해 모호한 설명을 가지고 있습니다. 그들의 문서는 기본적으로 예제 기반 (Z3)이거나 학술 논문으로 구성되어 실제로 구현 될 수도 실제로 구현되지 않을 수도있는 변경을 설명합니다.

나는 같은 1 차 논리의 decidable 조각 있다는 것을 알고

• 유한 한-경계는 수량이
• 단항 일차 논리

내가하고 싶은 무엇 FOL의 (있는 경우) 어떤 클래스가 완전한 SMT solver인지 알고 있습니까? 보고있는 문제가 그들이 완료 한 조각에 있는지 여부를 어떻게 알 수 있습니까?

Answer 1

CVC4가 완료되는 정량화 된 수식에는 두 가지 범주가 있습니다.

(1) 유한 도메인을 갖는 정량 된 수식.

CVC4는 해석되지 않은 정렬에 대한 한정 기호에 대해 유한 모델로 완성됩니다. 즉, 모든 해석되지 않은 정렬이 유한으로 해석되는 모델이 있으면 CVC4는 결국이를 찾습니다. 여기 컨퍼런스 논문을 요약
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
:이 기술은 CVC4 지원하는 모든 이론을 결합 할 것을
http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
공지 자세한 내용은이 논문을 볼 수 있습니다. 이론이 결정 가능하고 정량화가 (무한한) 해석 된 유형을 포함하지 않는다면, 유한 모델 완전성 보장이 남아있다.

Bernese-Schoenfinkel-Ramsey fragment (EPR)와 같은 특정 조각에 대해서도 논란이 있습니다. 즉,이 단편에서 문제가 해결되지 않으면 CVC4는 결국 "unsat"라고 대답 할 것입니다.

이 기능에 관심이있는 경우 CVC4는 기본적으로 입력 문제에 대한 유한 모델 찾기를 사용하지 않습니다. 명령 줄 옵션 "--finite-model-find"를 사용하면 이러한 기술을 사용할 수 있습니다.

(2) 한정어 제거를 방출하는 일부 이론의 정량 된 수식.

예를 들어, CVC4는 (순수한) 정량 선형 연산을 위해 완성되었습니다. Z3에서 예를 들어
http://homepage.divms.uiowa.edu/~ajreynol/cav15a.pdf

이, 다른 접근에 정신에서 유사하다 :
이전 회의 종이 기반으로 구축 http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
: 자세한 내용은이 논문을 볼 수 있습니다
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf

Answer 2

에서 도움이되지 않는 질문에 답하지 않을 위험성 때문에이 자료를 찾기가 어려운 이유가 있습니다.

결단력과 "실제로 기다릴 수있는 시간 내에 내 구체적인 문제를 해결할 수 있습니다"사이의 연결은 그렇게 강력하지 않습니다. 벤치 마크와 실험 결과의 예제가 더 자주 표시됩니다 (따라서 제시됩니다).

또한, 대부분의 솔버는 해결하기 전에 발견 재 작성 및 문제 조작의 양을한다. 다른 문제가 decieable들로 재 작성 될 수 decideable 조각을 표현 그래서 클래식, 구문 방법이 항상 적용되지 않습니다 (희망이 아닌 다른 방법으로 주위하지만 난 그런 일이 결코 약속 할 수있다!).

마지막으로, 많은 해법은 잘 작동하지만 코드보다 더 공식적인 뭔가 설명하기 어려운 휴리스틱 반 의사 결정 절차를 사용합니다. 따라서 알려진 결정 가능한 단편에는 나타나지 않을 수도 있지만 답변을 찾을 수있는 것들이 있습니다.