位置:成果数据库 > 期刊 > 期刊详情页
一种新的SAT问题预处理算法
  • ISSN号:1000-7180
  • 期刊名称:《微电子学与计算机》
  • 时间:0
  • 分类:TN47[电子电信—微电子学与固体电子学]
  • 作者机构:[1]复旦大学,专用集成电路与系统国家重点实验室,上海 201203
  • 相关基金:国家自然科学基金项目(90207002)
中文摘要:

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

英文摘要:

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.

同期刊论文项目
同项目期刊论文
期刊信息
  • 《微电子学与计算机》
  • 中国科技核心期刊
  • 主管单位:中国航天科技集团公司
  • 主办单位:中国航天科技集团公司第九研究院第七七一研究所
  • 主编:李新龙
  • 地址:西安市雁塔区太白南路198号
  • 邮编:710065
  • 邮箱:mc771@163.com
  • 电话:029-82262687
  • 国际标准刊号:ISSN:1000-7180
  • 国内统一刊号:ISSN:61-1123/TN
  • 邮发代号:52-16
  • 获奖情况:
  • 航天优秀期刊,陕西省优秀期刊一等奖
  • 国内外数据库收录:
  • 荷兰文摘与引文数据库,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:17909