1
저는 현재 다음과 같은 형식의 공식을 해결하기 위해 CVC4을 사용하고 있습니다 : 여기CVC4 : 한정어로 bool을 통해 함수를 합성하는 설정?
exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk)
의 f1...fn는 Bool 몇개의 기능이 Bool에, 그리고 b1...bk 부울 값입니다.
내 문제는 SMT의 UF 조각에 정면으로 내재되어 있습니다. 수량계는 있지만 함수 및 불린 이외의 다른 정렬은 없습니다.
CVC4의 기본 설정으로 문제를 해결할 때 모든 수량화가 유한 도메인을 초과 함에도 불구하고 즉시 알 수 없음을 반환합니다. 이 mbqi는 등의 난이 대부분에서 추가 된 인상을 얻을 cegqi의 무리, fmf의 무리가있다 : 문제는
는 CVC4는 한정사 처리하기위한 옵션의 매우 많은 수를 가지고 특정 연구 프로젝트가 아니라 내 솔루션을 얻으려고 20 가지 다른 논문을 읽지 않아도됩니다.
내 질문 : 이런 종류의 문제를 해결하기위한 권장 옵션이 있습니까?
CVT4는 SMT 대회의 UF Track에서 아주 잘 경쟁하고 수행했기 때문에 CVC4에서 가능하다는 것을 알고 있지만, 해당 경쟁에 사용 된 구체적인 주장을 찾을 수 없습니다.
우리는 비트 벡터를 사용하여 같은 문제에 직면 해 있습니다. – Greensheep