내가 시도 여러 SMT 솔버 (CVC3, CVC4 및 Z3) :SMT의 정량화 된 산술에서 추론의 한계는 무엇입니까? 다음과 같은 겉보기에 사소한 벤치 마크에서
(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall ((x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)
해결사 모두 알 돌아갑니다. 나는 이것이 결정할 수없는 조각 (잘 비선형)이라는 것을 이해하지만, 그것을 해결할 수있는 간단한 인스턴스 생성 방법이있을 것으로 기대하고 있었다. 나는 또한 상수와 함께 몇 가지 추가 단언을 추가하려했지만 도움이되지 않았다.
SMT에서 이러한 문제를 공격 할 수있는 방법과 정량화 된 산술에서 추론의 한계는 무엇입니까?
이 예제는 LIA (Linear Integer Arithmetic) 범주에 속합니다.
즉 Presburger Arithmetic은 qe 절차의 시간 복잡성이 매우 높지만 수량 한정자 제거 (qe)를 허용합니다.
내가 LIA에 대한 CVC3 및 CVC4 지원 정량 제거,하지만 Z3 당신이 Rise4Fun execution에서
(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall ((x Int)) (forall ((y Int)) (= y x))))
(check-sat-using (then qe smt))
을 할 수있는 확실하지 않다, 나는 unsat 결과를 가지고있다.
여기에서 qe 전술은 게임 종료 전술을 적용하기 전의 전처리 단계입니다. smt.
패드가 정확하면 qe 전 처리기가 상당히 비쌀 수 있습니다. 또한 VCC, Poirot, Dafny, VeriFast, Why3 및 ESCJava2과 같은 소프트웨어 확인 도구에서 나오는 수식에는 효과적이지 않습니다. 이 응용 프로그램에 의해 생성 된 수식에는 해석되지 않은 함수, 배열 등이 포함되어 있기 때문에 효과적이지 않습니다.
Z3은 답변을 제시하므로 Z3은 엔진 모음입니다. 사용자가 문제점을 해결하는 데 사용할 엔진 (또는 엔진 조합)을 선택할 수있는 API 및 명령을 제공합니다. 사용자가 (check-sat)이라고 말하면 입력 공식을 푸는 데 가장 좋은 엔진이 무엇인지 추측합니다. 추측은 사용자가 제공 한 입력 공식 및 주석의 구조 (예 : set-logic 명령)를 기반으로합니다. 우리는 자동 감지 된 조각 세트와 우리가 제공하는 엔진 세트를 지속적으로 확장하고 있습니다.
그런데 Z3가 LIA과 같은 조각을 놓치지 않고 자동으로 qe 절차를 적용하지 못하는 것은 당혹 스럽습니다. LIA 수식의 경우 일반적으로 qe이 가장 좋습니다. 전자 매칭이나 MBQI를 기반으로 한 대안은 완전히 다른 단편을위한 것이므로 효과적이지 않습니다.
LIA을 감지하는 committed code입니다 (set-logic을 사용하지 않은 경우에도 마찬가지 임). 변경 내용은 이미 unstable (작업중인 진행 중) 지점에서 사용할 수 있습니다. 야간 빌드 및 다음 공식 릴리스에서 내일 사용할 수 있습니다.