Hard satisfiable formulas for DPLL-type algorithms
Computational Complexity
2007-05-23 v1
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.
Cite
@article{arxiv.cs/0301012,
title = {Hard satisfiable formulas for DPLL-type algorithms},
author = {Sergey I. Nikolenko},
journal= {arXiv preprint arXiv:cs/0301012},
year = {2007}
}
Comments
9 pages