毕业论文
计算机论文
经济论文
生物论文
数学论文
物理论文
机械论文
新闻传播论文
音乐舞蹈论文
法学论文
文学论文
材料科学
英语论文
日语论文
化学论文
自动化
管理论文
艺术论文
会计论文
土木工程
电子通信
食品科学
教学论文
医学论文
体育论文
论文下载
研究现状
任务书
开题报告
外文文献翻译
文献综述
范文
SAT+MiniSAT三元可满足性问题的研究与实现(5)
表达式:表达式是多个子句的集合,当中的连接词是“并(AND)”,可以写成“&”。
下面是CNF的一个例子:
(x1 | -X5 | x4)&(-x1 | x5 | x3 | x4)&(-x3 | x4)。
MiniSat 能够接受的输入方式就是CNF格式,例子中就是这个格式,但是在输入的时候,要开头以“p cnf”,这就表示它接受的输入时cnf格式的,下面的所有例子里们都使用x作为变量,或者直接省略x,下面的是如入的格式:
P cnf 变量的个数 子句的个数
比如们变量的个数取5,子句的个数取3(都是随机的例子),就表示所有的变量为x1, x2, x3, x4, x5, -x1, -x2, -x3, -x4, -x5(们把这么多变量认为是5个变量,因为“-”只是一个变量的反变量),而子句的个数为3个,而且每一行的最后必须用0来代替,表示他们的关系是AND,那么上面的例子,MiniSat接受到的输入就是一个变量的取值个数为5,子句的个数为3的CNF SAT,如下:
P cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0
当运行MiniSat的时候,对于这个简单的例子,们知道这肯定不止一个解决方案,但是MiniSat只显示“SATISFIABLE”或者“UNSATISFIABLE”,这就是取决于这个SAT是否可解,但是如果你指定一个输出文件,那么MiniSat将会把输出结果写在这个文件中,第一行将会是“SAT(表示可解”或者“UNSAT(表示不可解)”,如果这个CNF是可解的,那么第二行将会给一个解决方案,即使有很多解决方案,MiniSat也只给出一个,在上述的例子中,假设上面的例子的文件名是“input.in"那么只要输入:
Minisat input.in output.out
MiniSat的运行结果就是显示在output.out中:
SAT
1 2 -3 4 5 0
这个表示这个CNF可解,解决方案是x1取真值,x2取真值,x3取非真值,x4取真值,x5取真值,所以解决原理如下(真=t,非真=f):
(x1|-x5|x4)=t|-t|t=t
(-x1|x5|x3|x4)=-t|t|f|t=t
(-x3|x4)=-f|t=t
所以t&t&t=t最终取值为真。
但是如果想要得到更多的解决方案,们可以在CNF中加入一个子句,子句的内容就是刚刚的解决方式的反方式:
P cnf 5 4
1 -5 4 0
-1 5 3 4 0
-3 -4 0
-1 -2 3 -4 -5 0
把这个放在名字为“second.in(名字自己取的)”的文件中,然后运行:
Minisat second.in second.out
们将会得到一个新的解决方案:
SAT
1 -2 -3 4 5 0
和之前一样,这个表示SAT可解,解决方案是x1取真值,x2取非真值,x3取非真值,x4取真值,x5取真值,所以解决原理如下
(x1|-x5|x4)=t|-t|t=t
(-x1|x5|x3|x4)=-t|t|f|t=t
(-x3|x4)=-f|t=t
所以最终t&t&t=t,最终取值为真。
4 SAT的可解性研究
4.1 前期操作步骤
在上一节中,已经能够通过生成器生成大量的3SAT合取范式,这一节,将会利用MiniSat解决器解答所需要的3Sat合取范式。
首先,下载了一个版本的MiniSat解决器(http://minisat.se/MiniSat.html),MiniSat C-v1.14.1,将其放入c盘中,这个版本的代码是通过C++语言编写的,所以要在电脑上安装Microsoft Visual C++ 6.0。在编译运行之后,MiniSat文件夹中将会出现一个“Debug”的文件夹。
然后,将上一节得到的3SAT合取范式放“Debug”文件夹中,便可以使用Minisat解决器解答,具体操作如下:
1.在xampp文件夹中打开xampp-control.exe,并把apache开始运行。
2.在浏览器中打开http://localhost/test/index.php,在网页上随机生成一个数据,比如v=4,c=16.文件序号为1,再点击“submit”,这样一个cnf文件已经生成在C:\xampp\htdocs\test里面,名字为output1.cnf,随机生成的元素个数为4,子句个数为16的3SAT合取范式,如下:
共7页:
上一页
1
2
3
4
5
6
7
下一页
上一篇:
ASP.NET基于WCF的通用权限管理系统的设计与实现
下一篇:
ASP.net+sqlserver在线留言板系统的设计与实现
公寓空调设计任务书
AT89C52单片机的超声波测距...
C#学校科研管理系统的设计
志愿者活动的调查问卷表
中国学术生态细节考察《...
承德市事业单位档案管理...
10万元能开儿童乐园吗,我...
神经外科重症监护病房患...
医院财务风险因素分析及管理措施【2367字】
国内外图像分割技术研究现状