DateSAT: 날짜 및 기간 제약 조건 해결을 위한 프레임워크

날짜와 달력 기간(즉, 일, 월, 년)은 소프트웨어, 데이터 및 문서 분석을 포함하는 작업에서 빈번하게 등장합니다. 이전 연구에 따르면, 날짜 및 달력 계산을 포함하는 컴퓨터 로직은 까다로운 규칙(예: 불규칙한 크기의 월), 모호성(예: "1월 31일"로부터 한 달 뒤의 일정 예약), 그리고 예외 케이스(예: 윤년)로 인해 오류가 발생하기 쉽다는 것이 밝혀졌습니다. 그러나 기존의 프로그램 분석 및 검증 도구들은 날짜에 대한 네이티브 지원(native support)을 제공하지 않아, 달력 산술(calendrical arithmetic)을 포함하는 연산을 기호적으로(symbolically) 추론하기 어렵습니다. 본 논문은 날짜 및 달력 기간을 포함하는 만족 가능성 제약 조건(satisfiability constraints)을 표현하고 해결하기 위한 최초의 프레임워크인 DateSAT을 제시합니다. 본 논문은 먼저 입력 언어와 날짜 및 기간 산술의 의미론(semantics)을 정형화합니다. 그런 다음, 정수(integers)를 포함하는 SMT 공식으로의 환원을 기반으로 DateSAT 제약 조건을 해결하기 위한 다섯 가지 별도의 전략을 제시하며, 이를 Z3를 백엔드(backend)로 사용하여 구현하였습니다. 우리는 LLM 프롬프팅(prompting), 문법 기반 샘플링(grammar-based sampling), 그리고 법률 문서 마이닝(mining legal documents)을 사용하여 합성된 450개의 DateSAT 제약 조건 데이터셋을 구축하였으며, DateSAT 솔버(solver) 성능에 대한 실증적 평가를 제시합니다.