一句话：提出基于双蕴含点的扩展归结子句学习算法，在CDCL SAT求解器中动态引入新变量，提升Tseitin与XOR类公式求解性能。
本文研究如何在冲突驱动子句学习（CDCL）SAT求解器中有效利用扩展归结（ER）来增强子句学习。作者提出ERCL算法，在求解器运行时构造的蕴含图中识别双蕴含点（DIP），并将DIP视为从最高决策层决策变量到冲突节点的一对支配节点；随后动态引入新变量作为这些DIP的定义，从而生成扩展归结学习子句。该方法实现于MapleLCM，称为xMapleLCM。实验将其与MapleLCM、Kissat 3.1.1、CryptoMiniSat 5.11、SBVA+CaDiL、以及GlucoseER等求解器比较，表明xMapleLCM在Tseitin和XORified公式上优于这些先进求解器，并对不同扩展归结实现进行了详细对比分析。
We present a new extended resolution clause learning (ERCL) algorithm, implemented as part of a conflict-driven clause-learning (CDCL) SAT solver, wherein new variables are dynamically introduced as definitions for {\it Dual Implication Points} (DIPs) in the implication graph constructed by the solver at runtime. DIPs are generalizations of unique implication points and can be informally viewed as a pair of dominator nodes, from the decision variable at the highest decision level to the conflict node, in an implication graph. We perform extensive experimental evaluation to establish the efficacy of our ERCL method, implemented as part of the MapleLCM SAT solver and dubbed xMapleLCM, against several leading solvers including the baseline MapleLCM, as well as CDCL solvers such as Kissat 3.1.1, CryptoMiniSat 5.11, and SBVA+CaDiCaL, the winner of SAT Competition 2023. We show that xMapleLCM outperforms these solvers on Tseitin and XORified formulas. We further compare xMapleLCM with GlucoseER, a system that implements extended resolution in a different way, and provide a detailed comparative analysis of their performance.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BussCGO26,
title = {Extended Resolution Clause Learning via Dual Implication Points},
author = {Sam Buss and Jonathan Chung and Vijay Ganesh and Albert Oliveras},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:23)2026}
}