본 논문은 대규모 작업에 대한 명시적 상태 공간 검색을 확장하는 데 있어 핵심 과제인 생성된 상태 집합을 압축하여 표현하는 방안을 제시한다. 모델 검사에서 사용되는 트리 데이터베이스를 동적으로 변형하여 명제 및 숫자 변수에 대한 상태 집합을 압축하며, 정적 트리 데이터베이스의 바람직한 속성을 유지함을 증명한다. 고전적 및 숫자 계획 문제에 대한 상태 압축 기술의 실험적 평가는 여러 차수의 압축률을 보이며, 런타임 오버헤드는 거의 무시할 수 있음을 보여준다.