---
title: "Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability"
authors:
  - "Nobuhiro Yugami"
doi: ""
url: "https://ijcai.org/proceedings/1995/37"
pdf: "https://ijcai.org/proceedings/1995/0037.pdf"
venue: "Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence"
year: 1995
pages: "282-287"
track: "Automated Reasoning"
keywords:
---

# Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability

Nobuhiro Yugami

*Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence*, 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.