SAT+MiniSAT三元可满足性问题的研究与实现(3)

        $y = rand(-$v,$v);//第二个元素命名为y，此处为第二个元素随机取数
while($x ==$y||-$x ==$y||$y==0)
{     $y = rand(-$v,$v);//此处第一个元素已经取数完成且符合要求，现在判断第二个元素与第一个元素绝对值不能相同，而且不为0，如果不合要求，则第二个元素重新取数
}
        $z = rand(-$v,$v);//第三个元素命名为z，此处为第三个元素随机取数
while($z == $x||$z == $y||$z ==-$x||$z==-$y||$z==0){
       $z = rand(-$v,$v);//此处第一个元素和第二个元素都已经取数完成而且符合要求，现在判断第三个元素，不能与第一个元素绝对值相同，而且不能与第二个元素绝对值相同，且不为0，如果不符合要求，则第三个元素重新取数
}
   $current = $x." ".$y." ".$z." 0\n";
   $final .= $current;//输出格式
}

file_put_contents("output" . $_POST['f'] . ".cnf",$final);//最终输出，输出文件名为output.cnf

?>
<a href="index.php">Input again</a>//这一句在此程序中没有取数的作用，是为了下一步与另一个程序连接而写，能使程序重新开始，进行第二个合取范式的取数。
2.2   生成器运行环境
这段程序是PHP语言，所以要在PHP环境中运行，即要在电脑上安装apache和mysql，但是由于机器硬件限制，安装这些环境会使电脑运行缓慢，最终会在进行3SAT的时间复杂性实验时，对实验结果有一定的影响。所以使用了简单的方法：使用xampp，让程序在网页中运行（省去了对apache的配置和安装）。
第一步，安装xampp在c盘中。
第二步，打开文件夹，运行其中的文件xampp-control.exe,运行后如下图2.2.1：

(图2.2.1)
只要用到apache所以只要将其中的apache打开即可：

(图2.2.2)
第三步，再次打开文件夹进入如下子文件夹C:\xampp\htdocs，在此文件夹中新建一个文件夹，取名为“test”然后进入，将刚才编写的程序（命名为cnf.php)放在此文件夹中。
第四步，在网页中运行此程序，打开浏览器网页http://localhost/test/cnf.php，网页可以运行如下：

(图2.2.3)
但是只能显示程序，但是不能输入，即不能生成3SAT合取范式。
第五步，为了配合这一程序，编写了一个网页程序来进行此程序的输入，程序如下：
<html>
<head><title>cnf</title></head>//网页标题
<body>
   <form action="cnf.php" method="post">//此处是使此网页能与上一程序连接，使程序在网页中运行
       <tr>
           <td>Input v:</td>
           <td><input type="text" name="v" /></td>／／输入元素个数ｖ
       </tr>
       <tr>
           <td>Input c:</td>
           <td><input type="text" name="c" /></td>／／输入子句个数ｃ
       </tr>
       <tr>
           <td>Input filenumber:</td>
           <td><input type="text" name="f" /></td>／／输出文件名编号，用来区分不同的３ＳＡＴ合取范式,如果此处输入1，则输出结果为output1.cnf SAT+MiniSAT三元可满足性问题的研究与实现(3):http://www.751com.cn/jisuanji/lunwen_1929.html