知行融创论坛第四期活动成功举办

基础软件与系统重点实验室党支部于 2025 年8月 27日成功举办了“知行融创”论坛第四期活动。本次活动聚焦基础软件与系统领域的核心算法与理论创新，四位同志带来了精彩的前沿研究分享，以下是报告的主要内容。

图为活动现场图片

1. 黄启凡. Efficient Formal Verification of Quantum Error Correcting Programs

Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers,and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coqproof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier,Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionalityof the framework by performing different verification tasks across various scenarios. Finally, we present abenchmark of 14 verified stabilizer codes.

图中为黄启凡

2. 李卓栋. A Divide-and-Conquer Approach for Global Orientation of Non-Watertight Scene-Level Point Clouds Using 0-1 Integer Optimization

Scene-level orientation of non-watertight point clouds remains an unsolved problem.We adopt a divide-and-conquer framework to address this challenge at the scene scale. The algorithm first partitions the point cloud into blocks, then estimates accurate normals in each block in parallel, and finally merges the blocks. To learn more about how we partition and merge subproblems, and how we adapt state-of-the-art iterative algorithms to non-watertight surfaces, we invite you to attend our presentation.

图中为李卓栋

3. 胡登杭. 含整数类型的字符串约束求解

含有复杂字符串处理函数，比如 replaceAll 和含整数类型的字符串约束求解是很有挑战性的问题，一般来讲是不可判定的。Chen 等人以符号执行为背景提出了字符串约束直线子集，并为该子集设计了基于有限自动机的判定算法，而且开发了字符串约束求解器 OSTRICH。OSTRICH 的一个局限是不能处理涉及整数数据类型的字符串约束，比如含有字符串长度、Substring、indexOf 的字符串约束。我们基于整数代价存储自动机对 OSTRICH 的判定算法进行了扩展，可同时处理字符串和整数数据类型，从而获得了含有以下字符串操作的直线子集的判定算法：连接操作、模式串为正则表达式替换串为常数串的 replaceAll 函数、reverse、函数转换器、字符串长度、Substring、和 indexOf。并实现了该判定算法，形成了原形工具。

图中为胡登杭

4. 姜滔. Separation between Walksat and DPLL

Modern SAT solvers can be broadly classified into two cate[1]gories. The first category comprises solvers based on the DPLL (Davis[1]Putnam-Logemann-Loveland) paradigm, which has achieved remarkable success with the combination of heuristics such as conflict-driven clause learning (CDCL) and restart mechanism. The second category consists of solvers employing the stochastic local search (SLS) approach, with Walksat being a prominent example. In this paper, we demonstrate that these two types of solvers can be distinguished by their performance on Tseitin formulas which have been extensively studied in proof complex[1]ity. Specifically, we show that Walksat can efficiently find a satisfying assignment for any satisfiable Tseitin formula with high probability in polynomial time. In contrast, we construct a family of Tseitin formulas on which any DPLL-based solver, even when enhanced with restarts, requires exponential time to find a solution. This analysis reveals a clear limitation of DPLL-based solvers compared to Walksat and suggests a potential direction for their improvements.

图中为姜滔

本期“知行融创”论坛围绕基础软件与系统领域的关键算法理论与技术突破，展示了实验室党员在并行计算、计算复杂性理论、形式化方法等前沿方向的创新成果。论坛持续为党员同志搭建了高水平的学术交流与思想碰撞平台，有效促进了不同研究方向间的交叉融合，生动实践了党建与科研业务的深度融合，激励党员在服务国家重大战略需求的科研一线攻坚克难、勇攀高峰。