Sam Buss ; Jonathan Chung ; Vijay Ganesh ; Albert Oliveras - Extended Resolution Clause Learning via Dual Implication Points

lmcs:15935 - Logical Methods in Computer Science, May 25, 2026, Volume 22, Issue 2 - https://doi.org/10.46298/lmcs-22(2:23)2026
Extended Resolution Clause Learning via Dual Implication PointsArticle

Authors: Sam Buss ; Jonathan Chung ; Vijay Ganesh ; Albert Oliveras

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.


Volume: Volume 22, Issue 2
Published on: May 25, 2026
Accepted on: April 13, 2026
Submitted on: June 25, 2025
Keywords: Logic in Computer Science

Consultation statistics

This page has been seen 1 times.