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.

翻译：我们提出了一种新的扩展推理子句学习(ERCL)算法，该算法作为冲突驱动子句学习(CDCL)SAT求解器的一部分实现，其中在求解器运行时构建的蕴含图中，新变量被动态引入作为{\it 双蕴含点}(DIPs)的定义。DIPs是唯一蕴含点的推广形式，可非正式地视为蕴含图中从最高决策层决策变量到冲突节点的一对支配节点。我们开展了大量实验评估来验证ERCL方法的有效性——该方法在MapleLCM SAT求解器中实现并命名为xMapleLCM——并与包括基线MapleLCM在内的多个领先求解器，以及Kissat 3.1.1、CryptoMiniSat 5.11和SAT竞赛2023冠军SBVA+CaDiCaL等CDCL求解器进行对比。结果表明xMapleLCM在Tseitin和XORified公式上优于这些求解器。我们进一步将xMapleLCM与采用不同方式实现扩展推理的GlucoseER系统进行对比，并对两者的性能进行了详细的比较分析。