SAT+MiniSAT三元可满足性问题的研究与实现(2)
时间:2017-01-06 13:21 来源:毕业论文 作者:毕业论文 点击:次
1.1 SAT的概念 首先，要先了解一下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.2 SAT的应用领域简介 SAT问题在硬件测试，人工智能，计算机视觉等很多领域都有广泛应用，对于自动电子设计领域的电路设计，FPGA路由，组合等式检测等问题的研究也极其重要。作为第一个被证明了的NP完全问题，长时间以来SAT问题求解方法得到了人们的不算改进，以期得到实际应用中可以接受的计算复杂度。 1.3 论文结构 本文基于SAT的可解性问题进行了研究，研究建立在理论知识的基础上，使用基本的ＳＡＴ解决器，对比较简单的SAT问题（即三元SAT：每个子句中只含有3个元素）进行解答，并对解答结果进行了分析，文章内容组织如下： 第２节介绍了三元ＳＡＴ的基本构成，解答原理，并使用ＳＡＴ生成器生成大量的ＳＡＴ合取范式；第３节介绍了本课题所要选择的ＳＡＴ解决器，以及对该解决器的原理及背景进行了介绍；第４节利用解决器对第一节中生成的大量的合取范式进行解答，根据解答结果（可解或者不可解）分类，并总结其中的规律；第５节在上一节的基础上，利用解决器对大量合取范式进行解答，并对解答结果中的时间复杂度进行记录分析，总结规律；第6节对本文中的操作过程以及结果做一定的说明，比如其中遇到的困难，失败并更正的情况，误差的分析等。 2 SAT生成器的特性以及运行环境 2.1 生成器代码简介 由于需要大量的3SAT合取范式，手动随机生成无法完成，所以根据上述所描述的3SAT组成元素K，V，C以及三者之间的关系，用PHP语言编写了一段程序来随机生成3SAT合取范式，程序如下： <?php $v = $_POST['v']; $c = $_POST['c'];//这两句是定义v，和c。 $final = "p cnf ".$v." ".$c."\n";//最后的输出格式 for ($i=0;$i<$c;$i++){ $x = rand(-$v,$v);//确定子句的个数为c个 while($x==0){ $x = rand(-$v,$v);}//第一个元素命名为x，此处循环表示x不能为0，为0时要重新取数 (责任编辑：qin) |