본 논문에서는 비선형 실수 산술 이론을 만족하는 문제(SMT-NRA)를 위한 하이브리드 프레임워크를 제안합니다. SMT-NRA에 대한 지역 탐색 기법의 핵심 연산인 cell-jump를 일반화한 2차원 cell-jump(2d-cell-jump)를 도입하고, 이를 통합한 확장된 지역 탐색 프레임워크인 2d-LS를 제시합니다. 탐색 효율을 향상시키기 위해 모델 생성 만족도 계산(MCSAT) 프레임워크를 통합하고, 실수 영역에서 CDCL 스타일 탐색에 적합하며 충돌 상태를 피하도록 돕는 sample-cell projection operator를 MCSAT에 구현합니다. 마지막으로, MCSAT, 2d-LS, OpenCAD를 통합한 SMT-NRA를 위한 하이브리드 프레임워크를 제안하며, 실험 결과를 통해 제안된 방법의 효과를 보여줍니다.
