EZSMTV3는 답집합 프로그래밍(ASP)에 제약 처리와 SMT를 결합한 CASP 문제를 SMT로 번역해 푸는 프레임워크의 3세대 버전이다. EZSMT+를 기반으로 더 표현력 있는 입력 언어, weak constraint를 통한 최적화 지원, 새로운 제약 타입 통합을 위한 확장 기반을 도입했다. 자체 탐색 절차 대신 CVC5, YICES, Z3 같은 최신 SMT 솔버에 추론을 맡기는 번역 접근을 취하며, 정수와 실수가 섞인 혼합 도메인 제약도 처리한다. CLINGCON, CLINGO[DL], CLINGO[LP] 등 동종 CASP 시스템과의 벤치마크 비교를 제공해, 선언적 조합 탐색 문제를 SMT 생태계의 발전에 얹어 풀려는 이들에게 견고한 플랫폼을 제시한다.

• •ASP+제약처리+SMT를 결합한 CASP를 SMT 번역 방식으로 푸는 EZSMTV3 설계·구현 발표
• •더 표현력 있는 입력 언어와 weak constraint 기반 최적화 지원, 새 제약 타입 통합 기반 추가
• •자체 탐색 대신 CVC5·YICES·Z3 등 최신 SMT 솔버를 백엔드로 활용
• •정수·실수 혼합 도메인 제약 처리 가능, CLINGCON·CLINGO[DL]·CLINGO[LP]와 벤치마크 비교 수록