该论文关注形式化验证与软件保障中的基础原语——UNSAT 证明（不可满足性证明）。在实际工程中，SAT/SMT 求解器生成的证明往往编码了专有逻辑、内部约束或安全敏感信息，直接公开披露会导致知识产权泄露或攻击面暴露。零知识 UNSAT 认证正是为化解这一矛盾而提出：证明者可在不泄露底层证明任何细节（除"该实例确实不可满足"这一结论外）的前提下，让验证者相信不存在可满足赋值。Luo 等人此前提出的 ZkUnsat 协议通过"在零知识下证明一个弱化后的归结（resolution）证明的有效性"来实现该目标，首次验证了零知识认证的可行性。然而其可扩展性受制于显著的证明者内存开销，难以处理真实规模的实例。本文受 LRAT 等高效明文 UNSAT 证明格式的启发，提出一种不引入额外泄露的预处理技术：将证明进行归一化，使每一条派生子句都由固定公开长度 k 的归结链来支撑。这一归一化既消除了链长度本身的侧信道泄露，又显著降低了证明者内存占用。在 SAT 2002 竞赛基准上，取 k=16 时，该方法比基线 ZkUnsat 多认证约 62% 的实例；在认证实例数量相同的情况下，内存占用降至基线的 25% 以下。该工作属于密码学与形式化方法交叉方向，适合零知识证明、形式化验证、隐私保护计算及安全审计工具的研究者与工程师阅读。