论文部分内容阅读
合取范式CNF（Conjunctive Normal Form）的可满足性SAT（Satisfiability）问题是人工智能、计算理论和理论计算机科学中的最瞩目问题之一.SAT问题的描述是非常简单的,但它是第一个被证明的NP完全问题,在计算复杂性理论中起着很重要的作用.同时该问题在自动推理、计算机辅助设计和制造、机器视觉、数据库、机器人、集成电路、计算机体系结构设计和计算机网络设计等许多实际问题中得到广泛的应用.该文的研究得到国家973重点基础研究发展规划项目“难解问题的高效实用算法及其应用”（NO.G1998030403）和国家教育部博士点基金（No.9703825）的资助.