首页 | 本学科首页   官方微博 | 高级检索  
     检索      

极小不可满足公式在多项式归约中的应用
引用本文:许道云.极小不可满足公式在多项式归约中的应用[J].软件学报,2006,17(5):1204-1212.
作者姓名:许道云
作者单位:贵州大学,计算机科学系,贵州,贵阳,550025
基金项目:中国科学院资助项目;贵州省高层次人才基金;贵州省省长基金
摘    要:合取范式(CNF)公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足,(r,s)-CNF是限制CNF公式中每个子句恰有r个不同的文字,且每个变元出现的次数不超过s次的公式类,对应的满足性问题(r,s)-SAT指实例公式限制于(r,s)-CNF.对于正整数r≥3,有一个临界函数f(r),使得(r,f(r))-CNF中的公式都是可满足的,而(r,f(r)+1)-SAT却是NP-完全的.函数f是否可计算是一个开问题,除了知道f(3)=3,f(4)=4外,只能估计f(r)的界.描述了极小不可满足公式在CNF公式类之间转换中的作用.为使转换过程中引入较少的新变元,给出了CNF公式到3-CNF公式的一种新的转换方法,对于长度为l(>3)的子句,仅需引入|l/2|个新变元.并且,给出了CNF到(r,s)-CNF公式转换以及(r,s)-CNF中不可满足公式构造的原理和方法.

关 键 词:极小不可满足公式  问题  多项式归约  NP-完全  公式构造
收稿时间:2005-06-15
修稿时间:2005-12-16

Applications of Minimal Unsatisfiable Formulas to Polynomially Reduction for Formulas
XU Dao-Yun.Applications of Minimal Unsatisfiable Formulas to Polynomially Reduction for Formulas[J].Journal of Software,2006,17(5):1204-1212.
Authors:XU Dao-Yun
Institution:Department of Computer Science, Guizhou University, Guiyang 550025, China
Abstract:
Keywords:minimal unsatisfiable formula  SAT-problem  polynomially reduction  NP-completeness  construction of formula
本文献已被 维普 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载免费的PDF全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号