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

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