# Subsumption-driven clause learning with DPLL+restarts

## TL;DR

This paper introduces a subsumption-driven clause learning method using DPLL with restarts, enabling efficient SAT solving and polynomial-time refutation of pebbling formulas, comparable to CDCL solvers.

## Contribution

It presents a novel approach combining subsumption-based clause learning with DPLL+restarts for efficient SAT solving.

## Key findings

- Refutes pebbling formulas in polynomial time and linear space.
- Achieves performance comparable to CDCL solvers.
- Demonstrates effectiveness of subsumption-driven clause learning.

## Abstract

We propose to use a DPLL+restart to solve SAT instances by successive simplifications based on the production of clauses that subsume the initial clauses. We show that this approach allows the refutation of pebbling formulae in polynomial time and linear space, as effectively as with a CDCL solver.