核心第一单元传播
Core First Unit Propagation
摘要：
自CDCL求解器开发以来，单位传播（也称为布尔约束传播）一直是每个现代CDCL SAT求解器的重要组成部分。一般来说，单元传播是通过在线性观察列表上顺序扫描每个子句来实现的。本文提出了一种新的单元传播技术，称为核心优先单元传播。其主要思想是在单元传播过程中优先选择核心子句而不是非核心子句，试图生成更短的学习子句。这里，核心子句被定义为文字块距离小于或等于7的子句。实证结果表明，核心第一单元传播提高了2018年SAT竞赛的获胜者MapleLCMDistChronoBT的性能。
英文摘要：
Unit propagation (which is called also Boolean Constraint Propagation) has been an important component of every modern CDCL SAT solver since the CDCL solver was developed. In general, unit propagation is implemented by scanning sequentially every clause over a linear watch-list. This paper presents a new unit propagation technique called core first unit propagation. The main idea is to prefer core clauses over non-core ones during unit propagation, trying to generate a shorter learnt clause. Here, the core clause is defined as one with literal block distance less than or equal to 7. Empirical results show that core first unit propagation improves the performance of the winner of the SAT Competition 2018, MapleLCMDistChronoBT.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
