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.

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