Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability
Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 282-287.
Abstract
This paper presents a statistical analysis of the Davis-Putnam procedure and propositional satisfiability problems (SAT} . SAT has been researched in AI because of its strong relationship to automated reasoning and recently it is used as a benchmark problem of constraint satisfaction algorithms. The Davis-Putnam procedure is a wellknown satisfiability checking algorithm based on tree search technique. In this paper, I analyze two average case complexities for the Davis-Putnam procedure, the complexity for satisfiability checking and the complexity for finding all solutions. I also discuss the probability of satisfiability. The complexities and the probability strongly depend on the distribution of formulas to be tested and I use the fixed clause length model as the distribution model. The result of the analysis coincides with the experimental result well.
@inproceedings{ijcai1995p37,
title = {Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability},
author = {Yugami, Nobuhiro},
booktitle = {Proceedings of the Fourteenth International Joint Conference on
Artificial Intelligence, {IJCAI-95}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Chris S. Mellish},
pages = {282--287},
year = {1995},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1995/37},
}
TY - CPAPER TI - Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability AU - Yugami, Nobuhiro T2 - Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI-95 PB - International Joint Conferences on Artificial Intelligence PY - 1995 SP - 282 EP - 287 UR - https://ijcai.org/proceedings/1995/37 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
