摘要
给出并证明了可满足性问题有解的一个充分必要条件,即合取范式的成假赋值仅由与简单析取式个数相等的有限个向量决定.在此条件基础上设计出用这些向量对初始赋值进行筛除的可满足性问题过滤算法,该算法的时间复杂性仅与向量个数和维数有关.为了在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.
出处
《华中科技大学学报（自然科学版）》
EI
CAS
CSCD
北大核心
2009年第7期75-78,共4页
Journal of Huazhong University of Science and Technology(Natural Science Edition)
基金
国家自然科学基金资助项目(60574041)
湖北省自然科学基金资助项目(2007ABA407
2005ABA233)
湖北省优秀中青年科技创新团队计划资助项目
湖北省教育厅A类项目(2004D005)
湖北省教育厅重点科研项目(D20091805)
关键词
可满足性问题
闭环DNA计算模型
过滤算法
删除实验
接入实验
SAT （satisfiability） problem
closed circle DNA computing model
filtering algorithm
delete experiment
insert experiment
