SAT+MiniSAT三元可满足性问题的研究与实现(5)
时间:2017-01-06 13:21 来源:毕业论文 作者:毕业论文 点击:次
表达式：表达式是多个子句的集合，当中的连接词是“并（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合取范式，如下： (责任编辑：qin) |