一种新的SAT问题预处理算法
提出了一项新的正向推理技术:对称扩展的一元子句推导(Symmetric Extended Unit Propagation).与传统的一元子句推导技术相比,文中的方法通过在一元子句推导过程中添加对称的蕴涵关系从而能够推导出更多的一元子句.基于这项新技术实现了一个可满足性问题(SAT)预处理器Snowball.实验结果验证了该项技术的有效性,表明该预处理器Snowball能够有效地化简SAT问题的规模并减少解决SAT问题的时间.
可满足性问题 一元子句推导 蕴涵图 预处理算法
熊伟 唐璞山
复旦大学,专用集成电路与系统国家重点实验室,上海,201203
国内会议
南宁
中文
193-196
2007-10-12（万方平台首次上网日期，不代表论文的发表时间）