【摘 要】
：
对于SAT求解器,目前流行的分支变量决策策略大多是基于冲突的变量活跃度评估算法,选择具有最大活性的未赋值变量作为决策变量,优先解决最近的冲突.但是,它们都忽略了包含决策变量的子句数目对布尔约束传播(BCP)的影响.针对此问题,提出了 一种基于学习子句删除策略的分支变量决策策略(VDALCD),在删除学习子句的同时减小被删除子句中变量的活跃度.基于VDALCD策略分别对Glucose4.1,MapleLCMDistChronoBT-DL-v2.1进行改进,形成了求解器Glucose4.1_VDALCD和Ma
【机 构】
：
西南交通大学数学学院 成都610031;系统可信性自动验证国家地方联合工程实验室 成都610031
论文部分内容阅读
对于SAT求解器,目前流行的分支变量决策策略大多是基于冲突的变量活跃度评估算法,选择具有最大活性的未赋值变量作为决策变量,优先解决最近的冲突.但是,它们都忽略了包含决策变量的子句数目对布尔约束传播(BCP)的影响.针对此问题,提出了 一种基于学习子句删除策略的分支变量决策策略(VDALCD),在删除学习子句的同时减小被删除子句中变量的活跃度.基于VDALCD策略分别对Glucose4.1,MapleLCMDistChronoBT-DL-v2.1进行改进,形成了求解器Glucose4.1_VDALCD和Maple-DL_VDALCD.以2018年、2019年SAT国际竞赛题为基准测试例,将改进版本与原版本求解器进行比较.实验结果表明,在2018年的例子测试中,Gluose4.1_VDALCD比Gluose4.1多求出26个例子,增加了 15.5％.在2019年的例子测试中,Maple-DL_VDALCD 比 MapleLCMDistChronoBT-DL-v2.1 多求出 17个例子,增加了 7.6％.
其他文献
针对个性化推荐,常用的推荐算法有内容推荐、物品协同过滤(Item CF)和用户协同过滤(User CF),但是这些算法以及它们的改进算法大多偏向于关注用户的显性反馈(标签、评分等)或评分数据,缺少对多维度用户行为和行为顺序的利用,导致推荐准确率不够高及冷启动等问题.为了提高推荐精度,文中提出了一种基于知识图谱的行为路径协同过滤推荐算法(BR-CF).首先根据用户行为数据,考虑行为顺序创建行为图谱(behavior graph)和行为路径(behavior route),然后采用向量化技术(Keras To
推荐系统缓解了互联网数据量剧增带来的信息过载问题,但传统的推荐系统由于数据稀疏和冷启动等问题导致推荐算法的准确性不高.因此,文中提出了一种基于知识图谱和标签感知的推荐算法(Knowledge Graph and Tag-Aware,KGTA).首先,利用项目和用户标签信息,通过知识图谱表示学习捕获低阶与高阶特征,将两个知识图谱中实体和关系的语义信息嵌入低维的向量空间中,从而获得项目和用户的统一表示.其次,分别利用深度神经网络和加入注意力机制的递归神经网络来提取项目和用户的潜在特征.最后,根据潜在特征预测评
在给定的任务中分析各种数据时,目前大多数研究只针对单源数据进行分析,缺乏应用于多源数据的方法.但如今数据日益丰富,因此提出一种多源数据融合框架,用于融合多种网络平台数据.同一平台数据中包含文本与各种属性,同时不同平台的数据在内容与形式方面也存在很大差异.然而现有的网络信息挖掘方法大多仅使用同一平台中的部分数据进行分析,忽略了不同平台的数据之间存在的相互作用.因此文中提出一种数据融合框架,一方面,能基于图的强大表示能力融合同一平台不同类型的特征,从而提升单个平台的任务性能;另一方面能够利用不同平台的数据特征
空间co-location(并置)模式是一组空间特征的子集,其实例在空间中频繁地邻近出现.由于空间数据同时存在关联性和异质性,co-location模式实例的分布或在整个研究区域中全局出现(全局co-location模式),或在研究区域的局部区域出现(区域co-location模式),从而提出了多级co-location模式挖掘.当前的多级co-location模式挖掘方法存在两个问题:1)已有的多级co-location模式挖掘方法忽略了模式在空间中的分布特性,未能准确区分全局和区域co-locatio
现有的物体姿态估计方法无法提供具有帧间稳定性的估计姿态,导致将其结果直接用于增强现实等可视化场景时会引起画面抖动,不适用于人机协同等应用场景。文中提出了一种包含多种方式的物体姿态估计优化方法,通过对原始姿态估计方法的损失函数的改进,并使用因果滤波的方法优化姿态估计结果,以获得具有稳定性的估计姿态。此外,为完善对姿态估计方法稳定程度的评价体系,文中提出了直接偏差距离DBD、方向反转率DRR与平均位移
平滑处理是数字图像去噪和产生模糊效果的重要手段,经常被用于美化润饰"伪造"图像,因此对各种平滑滤波实施检测是十分有必要的。针对常见的图像平滑处理,文中提出了一种新的基于差分直方图中尾部信息的平滑滤波检测算法。首先,针对待检测图像,基于不同差分步长和方向构建多个差分绝对值直方图;然后,提取直方图中差分值为0和1的出现频率,以及直方图尾部从大到小若干个差分值及其出现频率构建多维检测特征;最后,构建SV
随着卷积神经网络深度的不断增加,深度卷积神经网络的训练会变得更加困难。此外,在图像超分辨率中,低分辨率图像的通道特征和输入通常在不同的通道中被平等对待,这就导致了卷积神经网络的表征能力被弱化。为了解决这些问题,提出了一种多跳连接残差注意网络,该网络利用多跳连接中的残差(Residual in Multi-skip Connection, RIMC),构造了具有多个残差组的深度网络。每个残差组包含了
针对目标检测时Haar-like特征值过多、计算时间长、无法描述目标纹理特征且识别率一般的问题,提出一种基于滑窗原点信息的阈值自调节IHL(Improved Haar-like LBP)特征提取算法。该算法首先构造了IHL特征编码方法,将Haar-like特征和局部二值LBP特征融合;然后在计算Haar-like型局部二值化特征时,使用高斯矩阵获得符合像素分布规律的自调节阈值;同时在求特征值时引入
精细化的领域文本分析是高质量领域知识获取的重要前提,它通常依赖于大量某种形式的语义文法产生式,但总结这些文法通常耗时耗力.对此,文中提出了 一种基于容错Earley解析算法的语义文法自动学习方法,根据种子文法自动生成新的语义文法(包括词类和文法产生式),以减少人工成本.该方法利用优化后的容错Earley解析器,对输入的语句进行容错解析,然后根据容错解析生成的解析树产生候选语义文法,最后对候选语义文法进行过滤或纠正得到最终的语义文法.在5种不同疾病的中医医案的实验中,该方法的词类学习的正确率达到63.88％
尽管基于卷积神经网络的去雾算法在合成的均匀雾气数据集上已经取得了巨大进展,但在真实的非均匀有雾图像上仍然表现不佳。为了快速有效地去除图像中的非均匀雾气,文中首先提出了一种多补丁和多尺度层级聚合网络结构(Multi-patch and Multi-scale Hierarchical Aggregation Network, MPSHAN),融合了多补丁局部化信息和多尺度全局化信息。其次,提出了层级