Davis–Putnam algorithm: Difference between revisions

Revision as of 20:49, 19 October 2006

Revision as of 20:53, 19 October 2006

Line 1:

The '''Davis–PutnamDavis-Putnam algorithm''' was developed by [[Martin Davis]] and [[Hilary Putnam]] for checking the [[Boolean satisfiability problem|satisfiability]] of [[propositional logic]] formulae in [[conjunctive normal form]], ''i.e.'', sets of [[Clause (logic)|clauses]]. It is a form of [[resolution (logic)|resolution]] in which variables are iteratively chosen and removed by resolving every clause in which the variable is contained positively with any clause in which the variable is negated.

The algorithm works as follows:

Line 13:

==References==

* {{cite journal

|last=Davis

|first=Martin

| authorlink= Martin Davis

| coauthors= [[Hillary Putnam|Putnam, Hillary]]

| title=A Computing Procedure for Quantification Theory

| journal =[[Journal of the ACM]]

| volume = 7

| issue = 1

| pages = 201–215

| date = 1960

| url = http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=321034}}

*{{cite journal

* M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. ''[[Communications of the ACM]]'', 5(7):394–397, 1962.

| last=Davis

| first=Martin

* M. Davis and H. Putnam. A computing procedure for quantification theory. ''[[Journal of the ACM]]'', 7:201–215, 1960.

| coauthors=Logemann, George, and Loveland, Donald

| title=A Machine Program for Theorem Proving

| journal =[[Communications of the ACM]]

| volume=5

| issue=7

| pages = 394–397

| date=1962

| url=http://portal.acm.org/citation.cfm?doid=368273.368557}}

* R. Dechter and I. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In ''Proceedings of the Fourth International Conference on the Principles of Knowledge Representation and Reasoning (KR'94)'', pages 134–145, 1994.