基于频次的SAT问题学习子句混合评估算法

• 作者: 何星星 吴贯锋 常文静 徐扬 陈青山
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: SAT问题 并行求解器 LBD GLUCOSE
• 年，卷（期）: 2019,（8）
• 所属期刊栏目: 高性能计算
• 页码范围: 1374-1380
• 页数: 7页
• 分类号: TP311|TP391
• 字数: 5753字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2019.08.006

摘要

为了有效管理学习子句,避免学习子句规模呈几何级增长,减少冗余学习子句对系统内存占用,从而提高布尔可满足性问题SAT求解器的求解效率,需要对学习子句进行评估,然后删减学习子句.传统的评估方式是基于学习子句的长度,保留较短的子句.当前主流的做法一个是变量衰减和VSIDS的子句评估方式,另外一个是基于文字块距离LBD的评估方式,也有将二者结合使用作为子句评估的依据.通过对学习子句参与冲突分析次数与问题求解的关系进行分析,将学习子句使用频率与LBD评估算法混合使用,既反映了学习子句在冲突分析中的作用,也充分利用了文字与决策层之间的信息.以Syrup求解器(GLUCOSE 4.1并行版本)为基准,在评估算法与并行子句共享策略方面做改进测试,通过实验对比发现,混合评估算法比LBD评估算法有优势,求解问题个数明显增多.