中文摘要：

给出并证明了可满足性问题有解的一个充分必要条件,即合取范式的成假赋值仅由与简单析取式个数相等的有限个向量决定.在此条件基础上设计出用这些向量对初始赋值进行筛除的可满足性问题过滤算法,该算法的时间复杂性仅与向量个数和维数有关.为了在DNA计算模型上实现可满足性问题过滤算法,采用2n维向量的数据结构进行DNA编码代表可满足性问题的赋值;而闭环DNA计算模型的删除实验恰好能够完成对初始赋值的筛选,得到可满足性问题的可行解.最后用闭环DNA计算模型实现了可满足性问题过滤算法,并用实例说明了算法的有效性和可行性.

英文摘要：

A sufficient and necessary condition for SAT problem having solutions is put forward. It is proved that the false valuation of conjunctive normal form is determined by a finite number of vectors, whose number is equal to the number of simple disjunction. On the basis of this condition, filtering algorithm of SAT problem is designed for initial valuations to filter out using these vectors, whose time complexity is only related to the number of vectors and its dimension number. To realize filtering algorithm of SAT problem using DNA computing model, the data structure of 2n dimension vector is adopted to do DNA encoding, which represents a valuation of SAT problem, and delete experiment of closed circle DNA computing model can just complete selection of initial valuations to obtain feasible solutions of SAT problem. Therefore, filtering algorithm of SAT problem is realized by closed circle DNA computing model, and validity and feasibility of algorithm are explained with an example.