论文部分内容阅读
可满足性问题（SAT问题）在数理逻辑、人工智能、机器学习、约束满足问题、VLSI集成电路设计与检测以及计算机科学理论等领域具有广阔的应用背景。可满足性问题是第一个NP-完全问题，并且是一大类NP-完全问题的核心。大量的实践表明，许多NP-完全问题无论对于计算机科学理论还是工程应用都有着至关重要得意义。 极小不可满足公式的研究是近年来兴起的关于可满足性问题的一个热点方向。一个CNF公式F称为极小不可满足的（MU），如果F是不可满足，并且在F中删去任意一个子句后所得到的公式是可满足的。分裂技术是研究极小不可满足公式的很好工具。取出一变元x，我们对他进行真假赋值x=0和x=1，从而来考察赋值后得到的新的公式。对极小不可满足公式的一个变元赋值后，得到的公式仍是极小不可满足公式。特别地，可以使用分裂技术对公式归纳证明并对公式进行分类。 一对子句C1和C2是Hitting的，如果C1和C2中存在一对互补文字，即存在文字L使得L∈C1且（?）L∈C2。一个CNF公式F中的任意两个不同的子句中恰有一对互补文字，我们称F为非重言的Hitting公式（non-tautological hitting）。我们用NT-HIT表示非重言的Hitting公式类。 在[13]中，Hans Kleine Buning和赵希顺利用分裂技术研究了MU子类K的核K*，得出了K*在分裂下是封闭的结论。他们证明了NT-HIT-MU（k）=φ（k≥2）和MAX*=HIT-MU。同时，留下两个公开问题： （1）对于任意F∈NT-HIT（1）是否存在一个文字L，L在F中仅出现一次? （2）对于k≥2，NT-HIT（k）是否为空集? 本文根据NT-HIT所满足的条件，以公式的变元数n和子句数m为参数，构造了命题公式Hn,m。证明了： （1）Hn,m可满足当且仅当存在一个含有n个变元和m个子句的NT-HIT公式． （2）对于NT-HIT（1）中的任意一个公式F，存在文字L，L在F中仅出现一次． （3）对于k≥2，公式Hn,n+k是一个不可满足公式． （4）对于k≥2，NT-HIT（k）是一个空集． NT-HIT是一类重要的命题公式。Hn,m公式的构造不仅解决了长期困扰理论计算界的两个公开问题，而且从一个全新的角度、直观地诠释了NT-HIT公式类的结构与性质并完成了对其分类。