可满足性问题是一个寿命很长且经典的数学问题,SAT问题一般被称为命题逻辑的可满足性问题。确定性算法和非确定性算法是解决SAT问题的两种算法,为布尔表达式分配适当的逻辑值可以使公式为True,则称该公式是可满足的。根据给定的公式就可以检测出布尔可满足性问题是否可满足。在计算机的各个领域这个决策问题都至关重要,包括计算机科学,算法,密码学,人工智能和复杂性理论。建模这种方法适用于大多数的可满足性问题,高容量的存储、结果具有较高的精准度、最关键的一点是拥有高度的并行性,这些都是DNA计算所具有的优点,这就使得DNA计算在解决可满足性问题上占尽优势。可满足性问题的计算模型是本文的研究重点,并且这些模型的设计都是为了使DNA计算更加简便快捷,检测结果更为直观。文章主要分为四个部分,第一部分介绍了实验中比较多见的DNA分子操作技术,并且简单叙述了 DNA计算的一些基础知识,为后面介绍DNA计算模型打下了基础。第二部分对可满足性问题的基本知识作了介绍,包括算法,国内外研究进展。第三、四部分为文章的主要工作部分,分别介绍了两种不同的DNA计算模型。最后为本文的总结陈述部分。第三、四部分为本文的主要工作内容,介绍了两种基于DNA计算的可满足性问题的模型。第一种建立了一个基于DNA链置换的可满足性问题的计算模型,可满足性问题的约束条件被映射成计算模型上的荧光颗粒个数,将可满足性问题中变量的两种取值(0和1)分别设计成不同的DNA链,通过DNA链置换反应,最后观察找出满足可满足性问题的可行解,可以通过观察反应后的计算模型上的荧光颗粒个数得出,因为DNA链置换反应条件简单、所得到的产物量高,因此该计算模型具有一定的可行性,而且最后的结果通过荧光检测来观察反应的结果,操作简单、结果准确。但该计算模型的不足之处是模型建构比较简单,无法适用于更一般,规模更大的可满足性问题。第二种计算模型为一种动态的DNA折纸结构,该结构由DNA折纸卡槽、双态DNA机器、DNA行走机器人三部分组装而成。折纸卡槽由一条DNA长链和若干短链折叠而成,DNA行走机器人是由7条单链折成的三手四足DNA折纸结构,其中双态DNA机器可以控制阀门打开或者关闭,其结果就是DNA机器是否携带荧光颗粒。DNA机器人的“手”通过与双态DNA机器发生链置换反应接收其携带的荧光颗粒,机器人的“脚”在链置换反应的驱动下以顺时针旋转120°方向在折纸卡槽和DNA双态机器组装而成的折纸基底上完成行走。根据可满足性问题的约束变量选择性的接收荧光颗粒,每一步对应于一个变量的取值,以荧光团的个数映射问题的条件,以荧光团的颜色映射问题的解。两种模型都有操作简单易于观察检测的特点,因而大大提高了模型的可行性和计算的准确性。图[27]参[51]