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

基础软件与系统重点实验室党支部于 2025 年 4 月 23 日成功举办了知行融创论坛第一期活动。本次活动有四位同志进行了精彩的汇报交流，为与会人员带来了一场知识盛宴。

王踞秋同志对 #EO 问题的复杂性分类进行了深入研究。他研究了复数权重欧拉定向计数问题类（#EO）的计算复杂性，该问题在计数问题中具有重要地位。他给出了#EO问题类完整的复杂性二分定理，证明了由任意给定函数集合定义的 #EO问题，要么在FP^｛NP｝中，即可以多项式时间图灵归约到SAT问题，要么是#P难的。此外，作为#EO二分定理的推论，他还给出了由上偏、下偏和单一权重函数定义的Holant问题类的复杂性二分定理。

赵梦宇同志聚焦于基于动态变量级划分的分布式SMT求解技术。他指出，可满足性模理论（SMT）在许多关键领域中具有广泛应用，但现有技术在性能提升方面仍面临瓶颈，尤其是在分布式计算环境下的优化难题。为此，他提出了一种创新的分布式求解框架，基于动态变量级划分策略，将布尔传播与区间约束传播有效结合，显著提高了求解效率，同时，他还提出了一种高效的公式简化和搜索空间剪枝方法，并成功应用于CVC5、OpenSMT2和Z3等三大先进SMT求解器。经过测试，框架在整数和实数算术理论的多个测试用例中表现优异，尤其在非线性理论中表现突出。

薛白同志的报告介绍了一种用于刻画离散和连续随机系统无限时间安全概率上下界的数学约束构造方法。报告主要探讨了两种方法：第一种方法基于经典的Doob非负上鞅不等式。该方法放宽了现有研究中要求系统具有鲁棒不变集的限制，但无法用于构造安全概率上界的数学约束。第二种方法则源于薛白及其合作者前期提出的方程释放方法。该方法通过建立刻画准确安全概率的方程，并通过释放该方程获得安全概率上下界的数学约束。报告指出，两种方法在刻画安全概率下界时等价且具有充分必要性。而在刻画安全概率上界时，第二种方法更具普适性，填补了现有研究中缺乏刻画连续随机系统无限时间安全概率上界的方法的空白。此外，报告还简要介绍了针对多项式系统，利用半定规划方法求解这些数学约束，以及上述方法在有限时间和控制率生成方面的推广。

杨腾舜同志开展了基于 k–归纳的概率程序分段定量分析的研究。他提到在概率程序分析中，定量分析旨在为概率属性（如期望和断言概率）推导出紧致甚至精确的数值界限。为此，他提出了一种新的方法，用于生成紧凑的上下界，理论方面，他展示了如何从格化 k -归纳算子中提取有用的分段信息，并将分段信息与可选停止定理（OST）相结合，从而能够在概率程序中提取出分段约束；算法层面上，开发了生成分段多项式上下界的高效算法，并证明在线性情况下，生成问题可简化为双线性规划，而在多项式情况下，可正确地松弛为半定规划。实验结果表明，该方法生成的分段多项式界限在大量例子中表现良好。

本期知行融创论坛的成功举办，为党员同志们提供了一个学习交流、开拓视野的平台，促进了基础软件与系统领域的学术进步，以党建引领业务发展，充分激发了党员在科研工作中的先锋模范作用，为推动科技创新贡献了力量。