Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability
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. 1
Cite
Text
Yugami. "Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability." International Joint Conference on Artificial Intelligence, 1995.Markdown
[Yugami. "Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability." International Joint Conference on Artificial Intelligence, 1995.](https://mlanthology.org/ijcai/1995/yugami1995ijcai-theoretical/)BibTeX
@inproceedings{yugami1995ijcai-theoretical,
title = {{Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability}},
author = {Yugami, Nobuhiro},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1995},
pages = {282-288},
url = {https://mlanthology.org/ijcai/1995/yugami1995ijcai-theoretical/}
}