一种新的SAT问题预处理算法

• 作者: 唐璞山 熊伟
• 来源期刊: 微电子学与计算机
• 关键词: 可满足性问题 一元子句推导 蕴涵图
• 年，卷（期）: 2007,（10）
• 页码范围: 193-196
• 页数: 4页
• 分类号: TN47
• 语种: 中文
• DOI: 10.3969/j.issn.1000-7180.2007.10.058

摘要

提出了一项新的正向推理技术:对称扩展的一元子句推导(Symmetric Extended Unit Propagation).与传统的一元子句推导技术相比,文中的方法通过在一元子句推导过程中添加对称的蕴涵关系从而能够推导出更多的一元子句.基于这项新技术实现了一个可满足性问题(SAT)预处理器Snowball.实验结果验证了该项技术的有效性,表明该预处理器Snowball能够有效地化筒SAT问题的规模并减少解决SAT问题的时间.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	熊伟	复旦大学专用集成电路与系统国家重点实验室	11	66	6.0	8.0
2	唐璞山	复旦大学专用集成电路与系统国家重点实验室	36	143	7.0	9.0