【摘 要】
：
适当的重启有助于求解器跳出局部最优,但频繁重启会严重降低效率。为解决CDCL求解器重启触发条件随意性大的问题,提出一种基于搜索路径识别的延迟重启算法。该算法使用Luby序
【机 构】
：
西南交通大学信息科学与技术学院,系统可信性自动验证国家地方联合工程实验室
【基金项目】
：
国家自然科学基金项目（61673320,11526171,61305074）, 中央高校基本科研业务费项目（2682017ZT12）资助
论文部分内容阅读
适当的重启有助于求解器跳出局部最优,但频繁重启会严重降低效率。为解决CDCL求解器重启触发条件随意性大的问题,提出一种基于搜索路径识别的延迟重启算法。该算法使用Luby序列触发延时重启判断,将当前搜索路径和已搜索路径转换为向量空间模型,通过计算向量空间相似度来判断当前搜索过程是否会进入重复搜索空间。若向量空间相似度达到设定阈值,则触发重启,否则延迟重启。采用SAT国际竞赛的实例,与两个主流的求解器进行了对比实验。结果表明,所提算法能够有效规避重复搜索空间问题,并显著提高求解效率。
其他文献
采用连通支配集作为虚拟骨干可以延长无线传感器网络的生命时间,但是考虑到节点容易失效,虚拟骨干还需要具有一定的容错性。对此,针对任意k和m取值,提出了一种完全分布式的k-
采用部分主元素的Gauss消去法一般不能得到矩阵的各阶前主子式。讨论围绕逐步约化的细分每小步,对一个经过若干行置换后的A_0最后实现三角分解,并且依顺序求出A_0各阶前主子
通过对柞水县境内的红豆杉资源进行调查,摸清资源底数,对其生长生存环境进行分析,为今后资源保护及产业发展提出建议,以推动秦岭红豆杉的保护和发展。
随着现代教学理论的发展和进步,传统教学方式正在寻找不断拓展的新途径。高中语文教学在应试教育理念下逐渐不在适应社会发展的需要,对学生实际起到的指导作用有限,亟待寻找
针对状态事件故障树生成系统可达图过程中存在的状态空间爆炸问题,提出了一种基于时序关系的系统失效可达图生成方法。通过分析触发和被触发类型事件的时序关系,对存在时序关
推荐系统是解决信息过载问题和满足用户个性化需求的有效途径之一。然而,由于推荐系统需要用户提供不同程度的个性化信息来提升推荐的准确度,因此各种数据的安全问题成为阻碍
随着科学技术的蓬勃发展,数量众多的农机走进大众的视野中,让农户的生产生活变得比之前更加方便。农机在生产使用以后,其寿命会随着使用次数的增加而逐渐降低,所以加强对农机
21世纪初,随着我国对教育事业的关注度逐渐提升,中国的新课程改革工作进展迅速,而且在很多方面取得了新的突破,随着新课改的进一步实施,高职院校想要满足新课改提出的要求,就
传统养蜂产业是罗平县重点发展的特色经济产业,不仅能够带动农民增收,达到精准脱贫的目的,同时也能够推动罗平县经济发展。基于此,本文以罗平县为例,首先分析了传统养蜂产业
在并行计算机系统中,元器件和线路故障普遍存在,而系统的容错能力可以通过其底层基础网络的拓扑性质衡量。为了精确度量以k元n维冒泡排序网络为底层拓扑结构的并行计算机系统