Technical Summary: Extended Resolution Clause Learning via Dual Implication Points

Problem Statement

Conflict-Driven Clause-Learning (CDCL) SAT solvers have become ubiquitous in software engineering, security, and AI. However, despite their practical success, they are fundamentally limited by their reliance on the general resolution (Res) proof system, which is known to be weak for certain classes of formulas (e.g., Pigeonhole Principle, Tseitin formulas). While stronger proof systems like Extended Resolution (ER) exist and can provide polynomial-size proofs for these hard cases, integrating ER into CDCL solvers remains a significant challenge. Existing methods, such as GlucosER, introduce extended variables dynamically but rely on specific patterns of learned lemmas (consecutive lemmas sharing a common suffix) to identify new variables. The authors identify a need for a more flexible, general approach to dynamically introducing extended variables within the CDCL conflict analysis loop to improve solver performance on hard combinatorial problems.

Methodology

The paper proposes a novel algorithm for Extended Resolution Clause Learning (ERCL) implemented within the MapleLCM CDCL solver, resulting in a new system dubbed xMapleLCM. The core innovation is the use of Dual Implication Points (DIPs) to dynamically introduce new variables.

1. Dual Implication Points (DIPs)

A DIP is defined as a generalization of the Unique Implication Point (UIP). While a UIP is a single literal that dominates all paths from the highest decision level to the conflict node in the implication graph, a DIP is a pair of literals $\{x, y\}$ such that:

• Every path from the decision variable at the highest decision level to the conflict node passes through at least one node in the pair.
• Neither $x$ nor $y$ is a UIP.

The authors recast the problem of finding DIPs as finding Two Vertex Dominators (TVDs) in a directed graph. They utilize a linear-time algorithm (detailed in a companion paper [BGO24]) based on Menger's theorem and the identification of vertex-disjoint paths to find all valid DIP pairs efficiently.

2. ERCL Algorithm and Variable Introduction

When a DIP $\{a, b\}$ is identified during conflict analysis, the solver introduces a new extension variable $z$ defined as $z \leftrightarrow a \land b$. This allows the solver to learn two new types of clauses:

• Pre-DIP Clause: Derived from the implication that the first UIP and certain literals from previous decision levels imply the DIP pair. Formally: $\neg f \lor \neg C \lor z$ (where $f$ is the first UIP and $C$ represents literals leading to the DIP).
• Post-DIP Clause: Derived from the implication that the DIP pair and certain literals lead to a conflict. Formally: $\neg z \lor \neg D$.

This process effectively shortens the learned clauses by replacing complex conjunctions with a single variable, potentially reducing the search space.

3. Implementation and Heuristics

The authors implemented xMapleLCM as a highly extensible framework. Key heuristic decisions include:

• DIP Selection: Strategies include choosing the DIP closest to the conflict, the "middle" DIP (balancing the graph), or random selection.
• Filtering: Mechanisms to discard low-quality DIPs, such as requiring a minimum occurrence count (e.g., 20 or 50 times) or checking if the resulting post-DIP clause is a "glue" clause (LBD = 2).
• Clause Learning: Options to learn both pre- and post-DIP clauses or only the post-DIP clause.
• Variable Management: A strategy to delete extended variables that are no longer active (e.g., deleting the worst 50% of variables every 1000 conflicts) to prevent solver slowdown.
• Adaptive Switching: A heuristic that monitors the percentage of decisions made on extended variables. If this percentage drops below a threshold (3%), the solver reverts to standard 1-UIP learning to avoid overhead on instances where ER is not beneficial.

Key Contributions

1. Concept of DIPs: The introduction of Dual Implication Points as a generalization of UIPs, providing a new structural tool for analyzing conflict graphs.
2. Linear-Time Algorithm: An efficient algorithm for computing all DIPs in the implication graph, making the approach viable for runtime use in SAT solvers.
3. Flexible ERCL Framework: The development of xMapleLCM, a parameterizable system that allows developers to experiment with various DIP selection, filtering, and clause learning policies.
4. Empirical Validation: Extensive evaluation demonstrating that DIP-based ERCL significantly outperforms standard CDCL and other solvers on specific hard combinatorial benchmarks.

Experimental Results

The authors evaluated xMapleLCM against leading solvers (Kissat, CryptoMiniSat, SBVA-CaDiCaL, GlucosER) on four distinct benchmark families:

• Tseitin Formulas: On grid-based Tseitin formulas, xMapleLCM was the only solver to solve all instances within the 600-second time limit. While GlucosER performed well on regular Tseitin formulas, it struggled with grid-based instances. Standard CDCL solvers (Kissat, SBVA-CaDiCaL) performed poorly.
• Xorified Random k-XOR Formulas: xMapleLCM and GlucosER significantly outperformed other solvers. CryptoMiniSat, which uses Gaussian elimination, only succeeded on smaller instances or specific xorification settings, failing to scale on larger, harder formulas.
• Interval Matching Problems: For these unsatisfiable instances, no solver without extended resolution reasoning could solve any benchmark within a 2-hour limit. xMapleLCM and GlucosER solved all instances, with xMapleLCM being slightly slower but comparable.
• SAT Competition 2023 Main Track: On general benchmarks, xMapleLCM performed similarly to its base solver (MapleLCM). The adaptive switching mechanism successfully prevented performance degradation on instances where ER was not helpful, while still retaining the ability to solve hard ER-specific instances.

The authors note that approximately 63% of conflicts in their experiments contained at least one DIP, justifying the need for filtering mechanisms. They also observed that xMapleLCM and GlucosER identify different sets of extended variables (only ~25% overlap), suggesting they capture different semantic properties.

Significance and Claims

The paper claims that extended resolution can be successfully integrated into CDCL solvers to solve classes of formulas that are otherwise intractable for standard resolution-based solvers.

• Complementarity: The work demonstrates that there are multiple valid ways to automate ER (DIP-based vs. GlucosER's lemma-based approach), and both can be effective on the same hard problem classes.
• Practicality: The authors show that the overhead of detecting DIPs is negligible (typically <2.5% of runtime) and that the method does not degrade performance on general benchmarks when adaptive heuristics are used.
• Future Direction: The paper positions DIPs as a foundation for further research, including the exploration of $k$-Implication Points ($k > 2$) and the application of machine learning heuristics to better tune ERCL strategies.

The authors modestly conclude that while they have identified specific families where ERCL is superior, the theoretical question of whether DIP-based ER fully simulates unrestricted ER remains open and is a target for future theoretical investigation.