一种带有早期冲突检测的非-CDCL SAT求解器：基于监视文字的CSFLOC求解器
A Non-CDCL SAT Solver with Early Conflict Detection: The Watched-Literal-Based CSFLOC Solver
浏览论文内容
中文总结 AI 辅助
该研究提出基于监视文字的非-CDCL SAT求解器CSFLOC-WL3，通过早期冲突检测替换原CSFLOC的瓶颈搜索，实验显示其在近阈值随机3-SAT实例上优于对比求解器。
中文摘要 AI 辅助
CSFLOC是一种基于计数被包含的全长有序子句的非-CDCL SAT判定过程。经典CSFLOC循环通过一个单调计数器遍历全长子句的有序空间：若当前全长子句未被输入公式包含，则其否定式为一个可满足赋值；否则，一个包含子句会决定计数器跳转。主要瓶颈在于重复搜索此类包含子句。本文提出CSFLOC-WL及其当前实现CSFLOC-WL3，其中该搜索被替换为对计数器所表示的当前全长子句的否定式进行监视文字前缀传播。核心机制是早期冲突检测：若在公共前缀下的传播为同一变量导出相反的单位结果，则立即解析两个原因子句，并将该归结式用作新的计数器跳转原因。所得求解器不是CDCL求解器：它没有CDCL决策树、重启策略和第一UIP回跳循环。它仍然是计数器引导的全长子句计数求解器，但引入了监视文字数据结构和原因子句作为发现跳转的工程工具。对选定的UNSAT SATLIB实例进行的实验将CSFLOC-WL3与CSFLOC21TU和CaDiCaL 3.0.0进行比较，结果喜忧参半：CSFLOC-WL3在几个接近随机3-SAT可满足性阈值的随机3-SAT实例上表现强劲，而CSFLOC21TU在几个结构化案例上仍然更快，显然是因为它包含CSFLOC-WL3中尚未具备的更成熟的缓存机制。
英文摘要
CSFLOC is a non-CDCL SAT decision procedure based on counting subsumed full-length ordered clauses. The classical CSFLOC loop traverses the ordered space of full-length clauses by a monotone counter: if the current full-length clause is not subsumed by the input formula, its negation is a satisfying assignment; otherwise, a subsuming clause determines a counter jump. The main bottleneck is the repeated search for such a subsuming clause. This paper presents CSFLOC-WL, and its current implementation CSFLOC-WL3, in which this search is replaced by watched-literal prefix propagation over the negation of the current full-length clause represented by the counter. The central mechanism is early conflict detection: if propagation under a common prefix derives opposite unit consequences for the same variable, then the two reason clauses are resolved immediately and the resolvent is used as a new counter-jump cause. The resulting solver is not a CDCL solver: it has no CDCL decision tree, no restart policy, and no first-UIP backjumping loop. It remains a counter-guided full-length-clause-counting solver, but it imports the watched-literal data structure and reason clauses as engineering tools for discovering jumps. Experiments on selected UNSAT SATLIB instances compare CSFLOC-WL3 with CSFLOC21TU and CaDiCaL 3.0.0. The results are mixed: CSFLOC-WL3 is strong on several random 3-SAT instances near the random-3-SAT satisfiability threshold, whereas CSFLOC21TU remains faster on several structured cases, apparently because it contains a more mature cache mechanism that is not yet present in CSFLOC-WL3.
