View Related Documents

Abstract

The Davis and Putnam (D&P) scheme has been intensively studied during this last decade. Nowadays, its good empirical perfor- mances are well-known. Here, we deal with its theoretical side which has been relatively less studied until now. Thus, we propose a strictely lin- ear D&P algorithm for the most well known tractable classes: Horn-SAT and 2-SAT. Specifically, the strictely linearity of our proposed D&P algo- rithm improves significantly the previous existing complexities that were quadratic for Horn-SAT and even exponential for 2-SAT. As a conse- quence, the D&P algorithm designed to deal with the general SAT problem runs as fast (in terms of complexity) as the specialised algorithms designed to work exclusively with a specific tractable SAT subclass.

Keywords  Automated Reasoning - Computational Complexity - Search - Theorem Proving

Fulltext Preview

Image of the first page of the fulltext document