SAT+MiniSAT三元可满足性问题的研究与实现(4)
时间:2017-01-06 13:21 来源:毕业论文 作者:毕业论文 点击:次
</tr> <tr> <td colspan="2"> <input type="submit" name="submit" value="Submit" /> <input type="reset" name="reset" value="Reset" />／／确认提交，或者重新输入 </td> </tr> </form> </body> </html> 该程序命名为index.php,同样把该程序放在C:\xampp\htdocs\test中，然后打开网页运行http://localhost/test/index.php如下： (图2.2.4) 2.3 生成器操作及结果 假设，输入v=4，c=16，filenumber=88： (图2.3.1) 提交之后的文件输出结果为output88.cnf，并保存在C:\xampp\htdocs\test中： (图2.3.2) 打开盖输出文件夹，则可以看到，里面是一个元素取值范围为4，子句个数为16的cnf 3sat（下一节中将会介绍）合取范式： (图2.3.3) 上述步骤即为生成器的编写和使用步骤，如要得到大量3SAT合取范式，则只需要在Submit之后点击网页上出现的Input again，则会回到初始输入v，c，filenumber的页面，这段程序代码就是上述第一个程序cnf.php中最后一句话所实现的功能。 3 SAT解决器（SAT Solver） 3.1 SAT解决器的选择及特点 在此，选择了MiniSat Solver，因为MiniSat是一个比较简单的，而且是一个基于开原算法的SAT解决器，设计这个解决器的目的就是能够让研究者从这个解决器起步，去深入研究SAT。它是在麻省理工学院（MIT）发表的许可证，目前在很多项目上得到了应用。 首先，MiniSat从2003年就开始着力于通过向人们提供一个小巧的，有效的，并且能生成较好的文档的解决器来帮助人们从SAT入门。它的第一个版本只有600行的代码(不包括注释和空行），但是它却拥有有目前最先进的版本（2003版）的解决器的所有的功能以及特点。在以后的几个版本中，代码的数量有所增加，功能也有所提升，纵使如此，它本身还是非常的小，在2005年的SAT竞赛中，1.13版本的MiniSat解决器仍然被认为是最先进的解决器，至少在所有公开的版本中是这么认为的。 其次，MiniSat具有一切特殊的，其他解决器达不到的特点。第一点，它操作简单，容易修改，因为代码行数少，并且它生成的文档很容易理解，容易操作。它是被精心设计成一个理想的起点，用来让初学者适应SAT技术并理解SAT问题。第二点，它是一个高度有效的解决器，在2005年的SAT竞争中，在所有类别的解决器中获胜。MiniSat 解决器既能作为初学者用来入门的工具，又能作为一个应用程序来深入研究SAT。第三点：它的设计原理是为了适应整体性，他能够支持递增的SAT，而且它具有增加子句限制以外限制条件。它凭借着自身的易于操作的特点，成为了一个其他工具的整体上的基础工具，比如一个模型检查器，或者一个更多限制条件的解决器。 3.2 SAT解决器工作原理 MiniSat的工作原理很简单，们可以很容易就掌握，和其他许多解决器一样，MiniSat要求它的输入格式为合取范式（也就是CNF形式，或者cnf形式），CNF的促成板块如下： 元素：元素是指一个变量（比如x），或者一个反变量（比如-x）。 子句：子句是多个变量的集合，当中连接词是“或（OR）”，可以写成“|”，在同一个子句中，变量是不可以重复的。 (责任编辑：qin) |