互联网 qkzz.net
全刊杂志网:首页 > 女性 > 文章正文
刊社推荐

基于寻找可满足2-SAT子问题的SAT算法


摘 要:可满足问题(SAT)是一个NP-Hard问题。提出了一种求解SAT的新算法(FFSAT)。该算法将SAT问题转换为寻找一个可满足的2-SAT子问题。SAT问题虽然是NP完全问题,但是当所有子句长度不大于2时,SAT问题可以在线性时间求解。使用2-SAT算法-BinSat求解2-SAT子问题,当它不满足时,根据赋值选择新的2-SAT子问题。实验结果表明,采用本算法的结果优于UnitWalk。
  关键词:SAT问题; 2-SAT子问题; 2-SAT算法
  中图分类号:TP301.6
  文献标志码:A
  
  文章编号:1001-3695(2010)02-0462-03
  doi:10.3969/j.issn.1001-3695.2010.02.015
  
  New SAT solver based on finding satisfiable 2-SAT sub problem
  
  FU Yang-chun, ZHOU Yu-ren
  
  (School of Computer Science & Engineering, South China University of Technology, Guangzhou 510006, China)
  
  Abstract:Satisfiability (SAT) problem is one of the NP-Hard problems. This paper introduced a new SAT solver called FSSAT. This SAT solver solved the problem by searching a satisfiable 2-SAT sub problem. SAT was NP-complete, but it can be solved in linear time when the given formula contains only binary clauses (2-SAT).BinSat(2-SAT solver) was used to solve the 2-SAT sub problem and improved the 2-SAT sub problem according to the truth assignment. The experimental results show that the solver outperforms UnitWalk.
  Key words:SAT problem; 2-SAT sub problem; 2-SAT solver
  
  0 引言 ......
很抱歉,暂无全文,若需要阅读全文或喜欢本刊物请联系《计算机应用研究》杂志社购买。
欢迎作者提供全文,请点击编辑
分享:
 

了解更多资讯,请关注“木兰百花园”
分享:
 
精彩图文


关键字
支持中国杂志产业发展,请购买、订阅纸质杂志,欢迎杂志社提供过刊、样刊及电子版。
关于我们 | 网站声明 | 刊社管理 | 网站地图 | 联系方式 | 中图分类法 | RSS 2.0订阅 | IP查询
全刊杂志赏析网 2017