跳转至

文章背景与核心概要

本文介绍了在 Rocq 证明助手内对罗马诺夫三元组逻辑（Romanov's Triplet Logic, TLS）进行的首次机器化形式化。TLS 是一种专为布尔可满足性（SAT）设计的组合框架，建立在三元组结构和名为“简单顶点交集”（SVI）的过滤算法之上。该工作不仅形式化了 TLS 的完整核心，还明确了其复杂度和正确性边界，并通过提取 OCaml 原型推出了 VFR 工具链。

这项研究在计算机科学逻辑和人工智能领域具有重要意义，它通过超过 23,000 行代码和 424 个经过证明且零假设的引理，为 SAT 求解器的基础研究提供了坚实的机器可验证数学保证，展示了现代形式化方法在复杂组合算法验证中的强大威力。

罗马诺夫三元组逻辑的形式化验证：用于滑动窗口3-CNF的经验证过滤器及其在结构化公式中的应用 (Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas)

作者： Dmitry V. Alexandrov
学科： 计算机科学逻辑 (cs.LO)；人工智能 (cs.AI)；计算复杂性 (cs.CC)；程序设计语言 (cs.PL)
arXiv： 2608.18445v3 [cs.LO] | DOI： 10.48550/arXiv.2608.18445
提交时间： 2026年8月19日（最后修订于 2026年8月25日）

Authors: Dmitry V. Alexandrov
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Computational Complexity (cs.CC); Programming Languages (cs.PL)
arXiv: 2608.18445v3 [cs.LO] | DOI: 10.48550/arXiv.2608.18445
Submitted: 19 Aug 2026 (last revised 25 Aug 2026)

📌 摘要 (Summary)

本文在 Rocq 证明助手 中展示了对罗马诺夫三元组逻辑（Romanov's Triplet Logic, TLS）的首次机器化形式化。TLS 是一个专为布尔可满足性（SAT）设计的组合框架，构建于三元组结构以及名为简单顶点交集（Simple Vertex Intersection, SVI）的过滤算法之上。

This paper presents the first mechanized formalization of Romanov's Triplet Logic (TLS) within the Rocq proof assistant. TLS is a combinatorial framework designed for Boolean satisfiability (SAT), built on triplet structures and a filtering algorithm called Simple Vertex Intersection (SVI).

该工作的主要成就与贡献包括： * 核心形式化： 形式化了 TLS 的完整核心，涵盖 3-CNF 转换、清理过程以及 SVI 算法。 * 复杂性与正确性边界： 证明了良构滑动窗口片段过滤阶段的显式多项式时间界限。确立了精确的正确性边界：虽然 SVI 的非空性对于一般公式而言仅是必要的（但非充分的），但对于对齐结构证明了完全的双向蕴含（bi-implication），并将其推广到了结构系统。 * 分组窗口分析： 形式化了分组窗口转换，并提供了一个形式化的反例，证明了其不完全性。 * 工具链与产物： 推出了 VFR（罗马诺夫三元组逻辑经验证过滤器），这是一个提取出的 OCaml 原型，为滑动窗口片段提供了经过验证的判定过程，并为通用 3-CNF 提供了可靠的过滤器。该工具包含 Python 运行时、Docker 打包，并作为一个精选的 Zenodo 产物提供（DOI: 10.5281/zenodo.20397949）。 * 证明规模： Rocq 开发跨越了 23,000 多行代码，包含 424 个已证引理，且零未证明假设。

Key achievements and contributions of this work include: * Core Formalization: Formalized the complete core of TLS, encompassing 3-CNF translation, the clearing procedure, and the SVI algorithm. * Complexity & Correctness Boundaries: Proved explicit polynomial-time bounds for the filter stages of the well-formed sliding-window fragment. Established a precise correctness boundary: while SVI non-emptiness is merely necessary (but not sufficient) for general formulas, a full bi-implication is proved for aligned structures and extended to systems of structures. * Grouped-Window Analysis: Formalized the grouped-window translation and provided a formal counterexample demonstrating its incompleteness. * Toolchain & Artifacts: Introduced VFR (Verified Filter for Romanov's triplet logic), an extracted OCaml prototype providing a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF. The tool includes a Python runtime, Docker packaging, and is available as a curated Zenodo artifact (DOI: 10.5281/zenodo.20397949). * Proof Scale: The Rocq development spans over 23,000 lines of code, containing 424 proved lemmas with zero unproved assumptions.

📜 提交历史 (Submission History)

  • [v1] 2026年8月19日 星期三 – 02:20:59 UTC (41 KB)
  • [v2] 2026年8月21日 星期五 – 19:48:42 UTC (91 KB)
  • [v3] 2026年8月25日 星期二 – 16:37:46 UTC (49 KB) （当前版本，更新了 Zenodo 代码链接）
  • [v1] Wed, 19 Aug 2026 – 02:20:59 UTC (41 KB)
  • [v2] Fri, 21 Aug 2026 – 19:48:42 UTC (91 KB)
  • [v3] Tue, 25 Aug 2026 – 16:37:46 UTC (49 KB) (Current version, featuring updated Zenodo code links)