文献类型：期刊文章

作　　者：许道云[1]

机构地区：[1]贵州大学计算机科学系,贵州贵阳550025

出　　处：《软件学报》

基　　金：国家自然科学基金;贵州省高层次人才科研条件特助基金;贵州省省长基金~~

年　　份：2006

卷　　号：17

期　　号：5

起止页码：1204-1212

语　　种：中文

收录情况：AJ、BDHX、BDHX2004、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：2006289996323)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、ZMATH、核心刊

摘　　要：合取范式(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)的子句,仅需引入???2l???个新变元.并且,给出了CNF到(r,s)-CNF公式转换以及(r,s)-CNF中不可满足公式构造的原理和方法.

关 键 词：极小不可满足公式 问题  多项式归约  NP-完全  公式构造  

分 类 号：TP18]