본 논문은 일계 논리 문장의 모델 개수를 세는 문제인 일계 모델 계산(FOMC)에 대한 새로운 접근 방식을 제시합니다. 기존의 Crane 방법은 재귀적 함수 정의를 생성하여 모델 개수를 계산하지만, 수동으로 함수를 평가해야 하는 한계가 있었습니다. 본 논문에서는 Crane2라는 완전 자동화된 컴파일 알고리즘을 제안하여, 생성된 함수 정의를 임의 정밀도 연산을 지원하는 C++ 코드로 변환합니다. 이를 통해 기존 최첨단 기술 대비 50만 배 이상 큰 도메인 크기에 대해 FOMC를 확장할 수 있음을 실험 결과를 통해 보여줍니다.
