加权一阶 Horn 子句可满足性的搜索空间剪枝

基于摘要分析。本文研究统计关系学习（SRL）中以加权可满足性求解实现逻辑推理时的计算开销，提出针对一阶 Horn 子句的搜索空间剪枝算法；作者称该剪枝能够保留最优解，并报告搜索空间得到显著缩减。 原问题的主要瓶颈是：使用所有可能常量将子句完全实例化后再进行推理，计算成本较高。摘要将利用领域稀疏性的 LazySAT 作为相关背景，而本文选择限制知识库 Σ 的表达形式，仅考虑一阶 Horn 子句，以利用这一逻辑结构进行剪枝。摘要未提供具体剪枝规则，也不能据此认定实验中直接比较了 LazySAT。 理论方面，作者称证明了最优解必然存在于剪枝后的空间中；若存在满足知识库的模型，方法可在多项式时间内找到，否则寻找给定权重下最可能的解释。这里的“模型”指逻辑意义上满足子句的解释，而非预训练模型。多项式时间结论所依赖的输入表示、变量范围及其他适用条件尚未验证，不应外推为一般加权一阶逻辑推理的复杂度保证。 实验方面，作者报告搜索空间规模显著缩减，但摘要未给出数据、规模、缩减比例、运行时间或对照结果；实验协议、消融及统计信息尚未验证。材料研究对象是符号逻辑推理，未提供 EEG/BCI 信号建模机制或具体应用对应关系，因此不能将其视为已验证的 BCI 算法贡献。