본 논문은 하이브리드 SMT(Satisfiability Modulo Theory) 공식에 대한 모델 카운팅 문제를 해결하기 위해 pact라는 새로운 SMT 모델 카운터를 제시한다. 기존의 비트 블래스팅 기반 접근 방식은 이산 변수에만 국한되는 한계를 가지지만, pact는 해싱 기반 근사 모델 카운팅을 활용하여 이론적 보장 하에 해의 개수를 추정한다. pact는 투영 변수에 대해 로그 수준의 SMT 솔버 호출을 수행하며, 최적화된 해시 함수를 활용하여 성능을 향상시킨다. 대규모 벤치마크 실험 결과, pact는 기존 방식보다 월등한 성능 향상을 보였다. 예를 들어 14,202개의 인스턴스 중 pact는 603개를 성공적으로 처리한 반면, 기존 방식은 13개만 처리했다.
