SAT+MiniSAT三元可满足性问题的研究与实现.docVIP

SAT+MiniSAT三元可满足性问题的研究与实现 摘要：在学习计算机语言过程中，们经常遇到一些关系运算，其中用得比较多的是逻辑关系运算，为了对逻辑关系运算有进一步的深入了解，选择这个课题ldquo;三元可满足性问题的研究与实现rdquo;，对其可解性及解答时间进行研究，在研究过程中，对其中逻辑关系运算进行了解，能自己编写其子式结构，掌握其解决原理。 本论文运用两个工具：自行编写的SAT生成器和现成的MiniSAT解决器将SAT通过计算机生成并解答，从而得出解答结果，最后并对解答结果进行验证来进一步确定实验的准确性。 关键字：三元可满足性问题； SAT； MiniSAT；5057 设计说明书（论文）外文摘要 TitleThe study and realization of 3SAT Abstrack：In computing language,there are a lot of relational operations,and the most popular of which is logic operations.In order to know more about the logic operations,I choose the topic as my essay:Satisfiability.In the process of studying, we can learn to build the test bed of SAT,and we can also learn to solver the SAT with SAT Solver. There are two tools of this paper:SAT Creater and SAT Solver.In this paper,I use this two tools to create a test bed of SAT and solve them,in the process of creating and solving,by solving the possible situations of them,I get the conclution and I also test the conclution so as to make sure that it is ture. Keywords: SAT;MiniSAT 目次 1绪论3 1.1SAT的概念3 1.2SAT的应用领域简介3 1.3论文结构4 2SAT生成器的特性以及运行环境4 1.1SAT的概念 首先，要先了解一下3SAT的格式，以及这样的格式能不能用代码的方式实现，用代码的方式实现了，能不能实现用解决器解决这样的格式等等。 在计算机科学理论中，satisfiability（通常简称SAT）是一个决策性问题，给定一个布林方程式，是否存在一个变量在某种意义上使得这个方程式取值为真。3SAT合取范式是一个有一定格式的合取范式（CNF格式）：每个子句中的元素（变量的个数为3个。SAT解决器的功能就是能够接受这种格式输入的3SAT合取范式并解答。但是，目前为止，还没有一种解答器能够解答所有的3SAT问题，因为有些问题是相当复杂，并且结合实际，光解答器是无法解答的。这里所谓的复杂，并不是意味着3SAT中元素个数越多越复杂，子句个数越多越复杂，而是在一定的范围之内存在一定的规律。据调查显示，随机生成的3SAT合取范式中，们定义子句的个数用C（clauses）表示，元素的个数用V（variable）表示，而子句个数和元素个数的比值用K表示，也就是说K=C/V,当K处于2-6之间的时候，随机生成的3SAT是所有3SAT研究者起步时必经研究之路，因为在这个范围内，3SAT具有典型的规律并且难度也不是很小，而且在研究时也方便，因为在这个范围内的数据并不大，很适合初学者在普通电脑上就金额能进行研究操作。 不同的解决器能接受的3SAT格式不一样，所以下面所编写的程序输出的3SAT格式是根据选择的SAT解决器的格式而设定的，SAT解决器在下文中将做具体讲解。 1.2SAT的应用领域简介 SAT问题在硬件测试，人工智能，计算机视觉等很多领域都有广泛应用，对于自动电子设计领域的电路设计，FPGA路由，组合等式检测等问题的研究也极其重要。作为第一个被证明了的NP完全问题，长时间以来SAT问题求解方法得到了人们的不算改进，以期得到实际应用中可以接受的计算复杂度。 $y = rand(-$v,$v);//第二个元素命名为y，此处为第二个元素随机取数 while($x ==$y||-$x ==$y||$y==0) {$y = rand(-$v,$v);//此处第一个元素已经取数完成且符