毕业论文
计算机论文
经济论文
生物论文
数学论文
物理论文
机械论文
新闻传播论文
音乐舞蹈论文
法学论文
文学论文
材料科学
英语论文
日语论文
化学论文
自动化
管理论文
艺术论文
会计论文
土木工程
电子通信
食品科学
教学论文
医学论文
体育论文
论文下载
研究现状
任务书
开题报告
外文文献翻译
文献综述
范文
SAT+MiniSAT三元可满足性问题的研究与实现(4)
</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)”,可以写成“|”,在同一个子句中,变量是不可以重复的。
共7页:
上一页
1
2
3
4
5
6
7
下一页
上一篇:
ASP.NET基于WCF的通用权限管理系统的设计与实现
下一篇:
ASP.net+sqlserver在线留言板系统的设计与实现
公寓空调设计任务书
AT89C52单片机的超声波测距...
C#学校科研管理系统的设计
志愿者活动的调查问卷表
中国学术生态细节考察《...
承德市事业单位档案管理...
10万元能开儿童乐园吗,我...
神经外科重症监护病房患...
医院财务风险因素分析及管理措施【2367字】
国内外图像分割技术研究现状