论文部分内容阅读
可满足性（Satisfiability,SAT）问题是判定对于任意给定的一个合取范式（Conjunc-tive Normal Form,CNF）公式,是否存在对其变元的一个真值指派使得公式取值为真。该问题在人工智能、定理自动证明、集成电路设计、计算复杂性等领域有广泛应用。研究表明:当k≥2时,随机k-SAT问题具有以子句数与变元数的比值为参数的SAT-UNSAT相变现象。然而,对于正则（k,s）-CNF公式,该比值是s/k,即该比值对研究s取定的正则（k,s）-SAT问题不再适用。因此,本文提出了一个新的正则（k,s）-CNF公式类:严格d-正则（k,s）-CNF公式,它是指每个子句长度均为k,每个变元出现次数均为s,每个变元正、负出现次数之差的绝对值均为d的CNF公式。当d=0时,严格d-正则（k,s）-CNF公式退化为严格正则（k,s）-CNF公式。因为当s ≥ 4时,正则（3,s）-SAT问题仍然是NP-完全问题,所以,针对k=3的情形,研究了严格d-正则随机（3,s）-CNF公式的生成模型、难解性、可满足临界等,主要工作如下:（1）提出了用于生成严格d-正则随机（k,s）-CNF公式的SDRRKS模型,并且实验观察了 k=3时模型生成的随机公式的可满足性及求解难度。实验表明:在一定条件限制下,严格d-正则随机（3,s）-SAT问题具有SAT-UNSAT相变现象,其相变参数分别是s和d,而且s和d均影响严格d-正则随机（3,s）-SAT问题的求解难度。（2）研究了严格d-正则随机（3,s）-SAT问题的易解子类及NP-完全性。通过将极小不可满足公式用于多项式时间归约证明了:（a）严格s-正则（3,s）-SAT问题是易解问题;（b）对于s≥4,当s-4≤d≤s-2时,如果严格d-正则（3,s）-SAT问题存在不可满足实例,则该问题是NP-完全问题;（c）对于s>6,当0≤d≤s-6时,严格d-正则（3,s）-SAT问题是NP-完全问题。上述结论对严格d-正则随机（3,s）-SAT问题也成立。关于NP-完全性的结论给出了研究严格d-正则随机（3,s）-SAT问题的理论意义。（3）研究了严格d-正则随机（3,s）-CNF公式高概率不可满足的条件。使用一阶矩方法、多项式系数渐近近似技术、概率生成函数特定系数渐近近似技术等证明了:（a）对任给的d ≥ 0,存在实数s0,使得当s>s0时,严格d-正则随机（3,s）-CNF公式高概率不可满足;（b）对任给的s ≥ 12,存在实数d0,使得当d<d0时,严格d-正则随机（3,s）-CNF公式高概率不可满足。结论（a）和（b）分别支持实验观察到的以s为参数的SAT-UNSAT相变现象,以及以d为参数的相应相变现象;而数值结果验证了这两个结论的正确性。