毕业论文
计算机论文
经济论文
生物论文
数学论文
物理论文
机械论文
新闻传播论文
音乐舞蹈论文
法学论文
文学论文
材料科学
英语论文
日语论文
化学论文
自动化
管理论文
艺术论文
会计论文
土木工程
电子通信
食品科学
教学论文
医学论文
体育论文
论文下载
研究现状
任务书
开题报告
外文文献翻译
文献综述
范文
SAT+MiniSAT三元可满足性问题的研究与实现(2)
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问题(即三元SAT:每个子句中只含有3个元素)进行解答,并对解答结果进行了分析,文章内容组织如下:
第2节介绍了三元SAT的基本构成,解答原理,并使用SAT生成器生成大量的SAT合取范式;第3节介绍了本课题所要选择的SAT解决器,以及对该解决器的原理及背景进行了介绍;第4节利用解决器对第一节中生成的大量的合取范式进行解答,根据解答结果(可解或者不可解)分类,并总结其中的规律;第5节在上一节的基础上,利用解决器对大量合取范式进行解答,并对解答结果中的时间复杂度进行记录分析,总结规律;第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时要重新取数
共7页:
上一页
1
2
3
4
5
6
7
下一页
上一篇:
ASP.NET基于WCF的通用权限管理系统的设计与实现
下一篇:
ASP.net+sqlserver在线留言板系统的设计与实现
公寓空调设计任务书
AT89C52单片机的超声波测距...
C#学校科研管理系统的设计
志愿者活动的调查问卷表
中国学术生态细节考察《...
承德市事业单位档案管理...
10万元能开儿童乐园吗,我...
神经外科重症监护病房患...
医院财务风险因素分析及管理措施【2367字】
国内外图像分割技术研究现状