无阻断子模型的枚举
摘要：枚举不相交命题模型的基本算法(不相交的全真解析)是基于逐步添加阻塞子句来排除先前找到的模型。一方面，阻塞子句有潜力将生成的模型数量指数级地减少，因为它们可以处理部分模型。另一方面，它们需要指数级的空间并且减慢单位传播。我们提出了一种新方法，通过整合：冲突驱动子句学习(CDCL)，按时间顺序回溯(CB)，以及模型压缩方法(自反式压缩)，来实现对不相交部分模型的枚举，无需阻塞子句。实验清楚地显示了我们新方法的优势。
作者：Giuseppe Spallitta and Roberto Sebastiani and Armin Biere
论文ID：2306.00461
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-17