| 一种新的SAT问题预处理算法 |
| |
| 引用本文： | 熊伟,唐璞山. 一种新的SAT问题预处理算法[J]. 微电子学与计算机, 2007, 24(10): 193-196 |
| |
| 作者姓名： | 熊伟 唐璞山 |
| |
| 作者单位： | 复旦大学,专用集成电路与系统国家重点实验室,上海,201203 |
| |
| 摘 要： | 提出了一项新的正向推理技术:对称扩展的一元子句推导(Symmetric Extended Unit Propagation)。与传统的一元子句推导技术相比,文中的方法通过在一元子句推导过程中添加对称的蕴涵关系从而能够推导出更多的一元子句。基于这项新技术实现了一个可满足性问题(SAT)预处理器Snowball。实验结果验证了该项技术的有效性,表明该预处理器Snowball能够有效地化简SAT问题的规模并减少解决SAT问题的时间。
|
| 关 键 词： | 可满足性问题 一元子句推导 蕴涵图 |
| 文章编号： | 1000-7180（2007）10-0193-04 |
| 修稿时间： | 2007-06-02 |
A New Algorithm for SAT Preprocessing |
| |
| XIONG Wei,TANG Pu-shan. A New Algorithm for SAT Preprocessing[J]. Microelectronics & Computer, 2007, 24(10): 193-196 |
| |
| Authors: | XIONG Wei TANG Pu-shan |
| |
| Affiliation: | State Key Laboratory of ASIC and Systems, Fudan University, Shanghai 201203, China |
| |
| Abstract: | In this paper we propose a new forward reasoning technique called Symmetric Extended Unit Propagation (SEUP). Compared to the ordinary UP our method can deduce more unit literals through adding the symmetric implications during unit propagating literals. A SAT preprocessor Snowball is implemented based on this new technique. Experimental results verify the efficiency of this new technique and show that Snowball can generously reduce the overall runtime in solving SAT problems. |
| |
| Keywords: | satisfiability(SAT) unit propagation implication graph |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
