核心优先单元传播
计算机科学中的逻辑
2019-07-03 v1
摘要
单元传播（亦称布尔约束传播）自CDCL求解器发展以来，一直是各类现代CDCL SAT求解器的重要组成部分。通常，单元传播通过线性监视列表顺序扫描每条子句来实现。本文提出一种称为核心优先单元传播的新单元传播技术。其主要思想是在单元传播过程中优先处理核心子句而非非核心子句，以尝试生成更短的学习子句。此处，核心子句定义为字面块距离小于或等于7的子句。实证结果表明，核心优先单元传播提升了2018年SAT竞赛冠军MapleLCMDistChronoBT的性能。
引用
@article{arxiv.1907.01192,
title = {Core First Unit Propagation},
author = {Jingchao Chen},
journal= {arXiv preprint arXiv:1907.01192},
year = {2019}
}
备注
7 pages, 2 figures