UNSAT 증명은 정형 검증과 소프트웨어 보증의 표준 요소지만, 증명 자체가 독점적이거나 보안에 민감한 정보를 담을 때가 많아 공개가 부담스럽다. 영지식 UNSAT 인증은 증명자가 검증자에게 충족 불가능성만 확신시키고 그 외 정보는 노출하지 않게 해 이 긴장을 해소하며, 기존 ZkUnsat은 완화된 레졸루션 증명을 영지식으로 검증하는 방식으로 이를 구현했으나 프루버의 메모리 부담이 커 대규모 인스턴스로의 확장이 제한됐다. 이 논문은 LRAT 같은 효율적인 UNSAT 증명 포맷의 발전에 착안해, 추가 정보 유출 없이 ZkUnsat의 효율을 높이는 전처리 기법을 제안한다. 각 유도된 절을 고정된 공개 길이 k의 레졸루션 체인으로 정당화해 체인 길이 유출을 제거하고 프루버 메모리를 절감했으며, k=16일 때 SAT 2002 벤치마크에서 기존 ZkUnsat보다 약 62% 더 많은 인스턴스를 인증했고 동일 인증 수 기준 메모리는 25% 미만으로 줄였다.

• •영지식 UNSAT 인증의 프루버 메모리 부담을 줄이는 전처리 기법 제안
• •레솔루션 체인을 고정 공개 길이 k로 정규화해 체인 길이 정보 유출 제거
• •k=16 설정에서 SAT 2002 벤치마크 기준 인증 가능 인스턴스 약 62% 증가
• •동일 인증 수 기준 메모리 사용량을 기존 대비 25% 미만으로 절감