우리는 기존에 알려진 RECAR라는 접근 방식을 사용하는 방법과, modal resolution theorem prover인 KSP를 oracle로 사용하는 완전히 새로운 접근 방식을 모두 사용하여 CEGAR-tableaux를 SAT-shortcuts로 확장하는 두 가지 접근 방식을 조사합니다. 우리의 CEGAR-tableaux C++ 구현체인 CEGARBox++를 사용한 실험 결과는 다음과 같습니다: (1) RECAR SAT-shortcuts를 사용하는 CEGARBox++는 경쟁력이 없습니다. (2) SAT-shortcuts를 제공하기 위해 KSP를 사용하는 CEGARBox++는 CEGARBox++와 KSP 모두보다 우수하며, 특히 규모가 큰 satisfiable (충족 가능한) 문제에서 더욱 그러합니다. 우리가 아는 바로는, 이것은 modal satisfiability를 위해 SAT, tableaux, 그리고 resolution 방법론을 결합하여 각각의 개별 요소보다 더 나은 성능을 보이는 최초의 효과적인 통합 사례입니다.