SAT问题求解器重启策略对比分析

来源 :小型微型计算机系统 | 被引量 : 0次 | 上传用户:xiaoPhaiM
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
已有研究表明,在SAT求解器中引入重启可以极大地提高求解性能,并已出现了许多不同重启策略.目前还缺少全面的对比分析研究.为了避免重启策略选择的随意性,同时启发设计更好的重启策略,本文选择了具有代表性的7种重启策略,以目前广泛采用的Minisat为基本求解器,在国际SAT2011竞赛中实际应用类基准测试集之上进行了实验对比分析.结果表明:(1)不同重启策略对SAT求解器的求解过程和求解性能影响巨大;(2)在应用类测试集上,几何序列调度策略的平均综合性能优于其他策略;(3)在限定范围内,重启频率越大,求解器综合性能越好;(4)增量变化的重启频率可以克服固定重启频率导致不完备搜索的问题. Studies have shown that the introduction of restart in the SAT solver can greatly improve the performance of the solution, and many different restart strategies have emerged.At present, there is still a lack of comprehensive comparative analysis.In order to avoid the randomness of restart strategy selection, A good restart strategy, this paper chose a representative of the seven kinds of restart strategy, the widely used Minisat as the basic solver in the international SAT2011 competition practical application benchmark test set on the experimental comparative analysis results show that: (1) Different restart strategies have a great influence on the solving process and solving performance of the SAT solver; (2) On the application test set, the average synthesis performance of the geometric sequence scheduling strategy is superior to other strategies; (3) Within the limited range, The higher the restart frequency, the better the overall performance of the solver; (4) The incremental restart frequency can overcome the problem of incomplete search caused by the fixed restart frequency.
其他文献
现有的基于网的服务适配方法主要存在三个问题:需要借助Petri网的状态可达图来产生或验证服务适配器,这可能导致状态空间爆炸问题;都没有综合考虑语义层上的适配问题,仅能半
在当今大学生一方面困惑和远离文学阅读,一方面人文素养又有待提高的背景下,应该大力倡导经典文学阅读,以塑造大学生健康人格,提升大学生审美素养,培养大学生的创造性思维能
随着云计算的发展,互联网上涌现出越来越多的功能相同但服务质量(QoS)不同的Web服务.基于服务质量的服务推荐,旨在从这些等功能服务中挑选出满足用户服务质量需求的服务,已成
现实世界中新兴应用的快速发展导致各类数据的急剧增加,传统的数据挖掘模式已无法满足海量数据的需要,因此,本文提出一种基于动态云模型的树数据挖掘算法,以解决大规模树数据
在互联网环境中如何对分布、自治的服务进行有序化组织是一个挑战性问题.传统服务计算环境对服务的关系缺乏分析和有效管理,用户在构建应用时难以发现满足自己需求的服务.本
本文梳理了浪漫主义作为文学批评的术语,从二十世纪初引入中国以来,在中国古典文学和近现代文学研究中的流布,分析了浪漫主义在中国文学批评中误用的表现和原因,指明政治原因
支持替代的事务模型提供多条执行路径,提高了事务成功率.针对支持替代的事务模型,提出一种适于周期性事务的二重调度策略PT-DSS.外部调度中,PT-DSS采用固定优先级的可抢占调
复合事件探测是RFID事件处理的核心,本文对其中的非自发事件探测技术进行了深入研究,提出一种后继事件驱动的非自发事件探测方法 SD-EventD:SD-EventD将查询树中的非自发操作上提,与其父节点操作进行语义融合,直至最近的双目运算父节点;仅为双目运算符设置单队列,并基于单队列的后继事件驱动进行双目运算的语义探测;针对融合后的双目运算,给出了基于操作符语义的语义探测方法,即出入队规则.本文详
接到请求时,如何快速准确地查找满足用户需求的服务是服务发现的目的所在.现有的服务发现方法大都通过对服务功能属性的匹配计算来进行服务查找,对服务的过程模型并没有进行
Nutch是开源搜索引擎,Hadoop是Apache开发的类似于GoogleGFS和MapReduce的开源云平台.利用Nutch和Ha—doop可以设计高效、可靠、可扩展的搜索引擎,然而Nutch的分词模块对中文进