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.

In this paper, we explain how to improve Satisfaction-Driven Clause Learning (SDCL) SAT solvers by using a MaxSAT-based technique that enables them to learn shorter, and hence better, redundant clauses. A thorough empirical evaluation of an implementation on the MapleSAT solver shows that the resulting system solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver. Additionally we improve the understanding of the power of these solvers by proving that, given a refutation of a formula that consists of resolution and redundant-clause addition steps, an SDCL solver is able to produce a proof whose size is polynomial with respect to the size of the original refutation.