一个从k-CNF到t-CNF归约的有效算法

摘要

根据极小不可满足公式的特征,对于固定的3 ≤t＜k.我们给出了一个将k-CNF公式归约到t-CNF公式的有效算法.对于给定的k-CNF公式F,t-CNF公式的转换可以在公式F的长度的线性时间内完成.%By the characterizations of minimal unsatisfiable formulas, we present an effective algorithm for reducing the class k-CNF of formulas to the class t-CNF for fixed 3 ≤ t ＜ k. For given k-CNF formula F, the transformation of t-CNF can be completed in linear time on the size of F.