一种基于识别重复路径的动态决策策略

发布时间：2023-12-10 17:39

　　在现有基于冲突学习子句的求解器中,重启和变量相位存储技术的频繁应用,导致重启之后产生大量重复变量赋值序列,在求解过程中对变量重复赋值会浪费求解资源.本文提出一种基于识别重复路径的动态决策策略.首先,检测搜索过程中产生的重复赋值变量序列,算法中参数依据子句数与变元数的比率而动态变化;其次,更新参与冲突次数最多的变量的活跃值,选择合适的分支决策变量,改变变量赋值序列.本文基于国际SAT竞赛中知名求解器Glucose3.0,MapleCOMSPS,Glucose4.1以及Lingeling,分别实现了改进算法——DDIDT.实验结果可得,改进求解器Glucose_DDIDT相比Glucose3.0降低决策数为11.2%～61.6%,且Glucose_DDIDT求解难度较大实例的个数提高了63.9%.针对求解2015年到2017年SAT竞赛的应用类型的实例,Glucose_DDIDT相比Glucose3.0的求解个数增长了6.0%;改进求解器MapleCOMSPS_DDIDT相比MapleCOMSPS求解个数提高了...

【文章页数】：14 页

【文章目录】：
1 引言
2 基础知识
    2.1 基本概念
    2.2 CDCL算法
    2.3 重启策略
        2.3.1 静态重启策略
        2.3.2 动态重启策略
3 基于识别重复路径的决策策略
    3.1 重复赋值序列
    3.2 识别重复赋值序列
    3.3 动态改变赋值序列
4 实验与结果分析
    4.1 求解单个实例
    4.2 求解不同类型实例
    4.3 实验结果
5 总结
Background



本文编号：3872832