一个高效、健壮的SAT程序的研究与开发

来源 :上海交通大学 | 被引量 : 0次 | 上传用户:xxcoldrain
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
该文在探讨了SAT算法及其实现技术的基础上,描述了作者为了实现一个高效、健壮的SAT程序而进行的研究和实验工作,主要内容包括:第一,为了能够高效地实现SAT程序并能够在同等条件下比较各种不同的算法和技术,作者在总结前人成果和经验的基础上,结合自己的想法,设计了一个通用的基于DPLL的SAT程序框架:3D-DPLL框架.作者利用3D-DPLL框架来实现了自己的SAT程序,并且借助3D-DPLL作为测试台比较了几种分支决策策略和SAT算法;第二,作者实现了一个新的高效、健壮的SAT程序QuickSAT.在高效地集成了几种已经被证明了能有效提高SAT程序运行性能的算法策略.实验结果表明,在性能上,QuickSAT与当今世界上最高效的非商用完备类SAT程序zChaff相差无几,而在健壮性上比起几个当今最先进的SAT程序都要稍胜一筹,即QuickSAT能够在规定时间内解决更多的SAT问题.
其他文献
该文首先分析了人工服务难以建立统一应用逻辑规则的特点以及iCALL系统的特征,提出有限状态机建模的可定制流程机制以实现人工服务的可定制性.可定制流程机制的框架结构主要
Ad hoc网络作为一种无中心、自组织网络,因其不需要现有信息网络基础设施的支持,能够适用于战场、灾害、临时会议等特殊场合而成为研究热点。由于使用无线链路,分布式控制,网
离群点发现是数据挖掘的一项重要技术。本文提出了对高维空间下离群点挖掘技术上的一个改进,即利用粗糙集的约简特性对高维空间下的数据属性进行约简,通过约简一些无关紧要的属
从计算机诞生之日起,不断的追求更高的性能就成了计算机行业不变的主题。由大量处理器组成的高性能并行计算机的研究更是永远处于计算机领域的前沿,但是如何利用这些并行计算技
随着Internet进一步发展,人们对于Web应用软件的依赖性越来越高,Web应用软件的可靠性问题越来越引人关注。相关研究表明,Web应用软件中存在软件老化现象,Web应用软件老化的研
该论文是结合上海市教委发展基金项目进行的,前期工作基本上完成了协同编著系统的系统结构、协作机制、群组通信等研究,但是系统中还缺乏有效的版本管理控制手段以及全面的协
击键动态认证技术作为一种基于行为的生物认证技术,不仅具有一般生物认证技术(如指纹识别,人脸检测,虹膜认证等)的标识唯一性、随身性等特点以外,还具有成本低、简单方便、公
该文在深入研究面向对象技术(Object-Oriented Technique)、统一建模语言(Unified Modeling Language)、软件体系结构(Software Architecture)、设计模式(Design Pattern)、W
该文中,我们设计了基于XML的电子商务集成模型XECI.XECI提出了Internet上B2B商业交易的框架, 它对Internet上电子商务的C/S结构进行扩展,提出了三层结构;并在此基础上,通过对
无线传感器网络具有容易部署、可靠性高、可扩展等特点,在多个领域具有广泛的应用前景,是一种新兴的交叉研究领域。但由于网络结构和应用环境限制,节点所用的微型电池能源有