Hard satisfiable formulas for DPLL-type algorithms

TL;DR

This paper establishes exponential lower bounds on the time complexity of DPLL-type algorithms with heuristics when solving certain satisfiable formulas, highlighting fundamental limitations of these algorithms.

Contribution

It provides the first exponential lower bounds for DPLL algorithms with heuristics on provably satisfiable formulas, advancing understanding of their computational limits.

Findings

Exponential lower bounds for DPLL algorithms with heuristics

Limits on solving certain satisfiable formulas efficiently

Insights into the complexity of propositional satisfiability algorithms

Abstract

We address lower bounds on the time complexity of algorithms solving the propositional satisfiability problem. Namely, we consider two DPLL-type algorithms, enhanced with the unit clause and pure literal heuristics. Exponential lower bounds for solving satisfiability on provably satisfiable formulas are proven.