본 논문은 양자 컴파일 파이프라인에서 중요한 단계인 클리포드 회로 최적화에 대해 다룬다. 기존의 휴리스틱 기반 컴파일러는 속도는 빠르지만 최적이 아닌 결과를 생성하는 경우가 많다. 특히, 2-qubit CNOT 게이트와 같은 노이즈가 많은 게이트의 최소화는 실용적인 양자 컴퓨팅에 중요하다. 본 논문에서는 휴리스틱 접근 방식의 한계를 극복하기 위해 SAT 기반 접근 방식을 개선하여 CNOT 개수 최적화를 보장하는 클리포드 정규 형태 제한 검색을 통합한다. 병렬 계획을 허용하여 CNOT 깊이를 최적화하는 두 번째 SAT 인코딩을 제안하고, 하드웨어 플랫폼의 연결 제약 조건을 처리하고 큐비트 재라벨링을 허용한다. 개발된 알고리즘을 오픈소스 도구 Q-Synth에 구현하여 실험을 진행, 기존 SAT 접근 방식보다 성능이 뛰어나며, TKET 및 Qiskit 컴파일러와 비교하여 CNOT 개수 및 깊이를 최대 32.1% 및 48.1%까지 감소시키는 결과를 얻었다. 주요 양자 플랫폼의 연결 제약 조건을 고려한 실험에서도 Qiskit 대비 CNOT 개수 및 깊이를 최대 30.3% 및 35.9%까지 추가로 감소시켰다.
