命题逻辑中的L-型冗余性质

作者：刘凌荣; 陈树伟^*; 姜世攀

来源：计算机科学, 2023, 50(S1): 53-57.

• 命题逻辑
• 子句消去方法
• L-型冗余性质

在命题逻辑SAT求解过程中，子句集简化技术是重要的一个环节。冗余性质所对应的子句消去方法可以准确识别并删除冗余子句。无论是在预处理阶段还是SAT求解过程中，子句消去方法嵌入到SAT求解器均可加快求解器的求解效率。现有的高效子句消去方法大多基于封锁子句冗余性质和蕴涵模归结子句冗余性质扩展而来，为检查子句C是否冗余，只需要考虑子句C是否满足冗余条件。提出一种L-型冗余性质，它是封锁冗余性质、包含冗余性质、蕴涵模归结冗余性质的推广，将冗余子句判断条件由单个文字的归结式拓展到文字集合的组合。然后，针对L-型冗余性质，分析L-型冗余子句具有的性质，并将L-型冗余子句与已有的冗余子句的高效性进行比较，说明所提出的L-型冗余性质的高效性。

• 单位
  西南交通大学; 数学学院