Extended Resolution Clause Learning via Dual Implication Points

TL;DR

This paper introduces a novel extended resolution clause learning algorithm with dual implication points, integrated into a SAT solver, demonstrating improved performance on specific formula types through extensive experiments.

Contribution

The paper proposes a new ERCL algorithm using Dual Implication Points, implemented in the MapleLCM solver, and shows its effectiveness compared to existing solvers.

Findings

xMapleLCM outperforms several leading SAT solvers on Tseitin and XORified formulas.

The ERCL method with DIPs improves solver efficiency and conflict analysis.

Comparative analysis shows advantages over GlucoseER in certain benchmarks.

Abstract

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.