极小不可满足公式在多项式归约中的应用

• 作者: 许道云
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 极小不可满足公式 问题 多项式归约 NP-完全 公式构造
• 年，卷（期）: 2006,（5）
• 所属期刊栏目: 2005年中国计算机大会推荐优秀论文
• 页码范围: 1204-1212
• 页数: 9页
• 分类号: TP18
• 字数: 9297字
• 语种: 中文

摘要

合取范式(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中不可满足公式构造的原理和方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	许道云	贵州大学计算机科学系	125	460	12.0	16.0