| WHAT IS THE COMPARABLE DIFFERENCE OF DIFFERENT PROOF SEARCH TECHNIQUES.
|
| Formulated in a more concrete way, which is the best system (from a
| theoretical perspective !) to use to prove a propositional formula a
| tautology. This is not straightforward, as we are dealing with an NP
| complete problem.
ma_friesel@gate.pnl.gov remarks:
| Some techniques may be better for some categories of formulation than for
| others
Indeed, the Uribe & Stickel paper referenced below compares BDDs (which are
taking the world by storm in hardware verification) and the rather older
Davis-Putnam algorithm, and concludes that sometimes one is better, sometimes
the other, depending on the kind of problem considered.
You might look at Stalmarck's work, if you haven't already; his algorithm
(which is patented for commercial use) is allied to a theoretical
classification of tautological hardness. I'm not qualified to say how
significant his classification is in general (i.e. in isolation from his own
algorithm), but it's quite interesting.
A few references (in Bibtex format) to Davis-Putnam, BDDs and Stalmarck's
method are given below.
John.
* * * * * * * * * *
@ARTICLE{bryant,
author = "Randall E. Bryant",
title = "Graph-based Algorithms for {B}oolean
Function Manipulation",
journal = "IEEE Transactions on Computers",
year = 1986,
volume = "C-35",
pages = "677--691"}
@ARTICLE{bryant-survey,
author = "Randall E. Bryant",
title = "Symbolic {B}oolean Manipulation with
Ordered Binary-Decision Diagrams",
journal = "ACM Computing Surveys",
year = 1992,
volume = "24",
pages = "293--318"}
@ARTICLE{davis-putnam,
author = "Martin Davis and Hilary Putnam",
title = "A Computing Procedure for Quantification Theory",
journal = "Journal of the Association for Computing Machinery",
volume = 7,
year = 1960,
pages = "201--215"}
@ARTICLE{moore-bdds,
author = "J Moore",
title = "Introduction to the {OBDD} Algorithm for the
{ATP} Community",
journal = "The Journal of Automated Reasoning",
volume = 12,
year = 1994,
pages = "33--45"}
@INPROCEEDINGS{stalmarck-safecomp90,
crossref = "safecomp90",
author = "Gunnar St{\aa}lmarck and M. S{\"a}flund",
title = "Modeling and Verifying Systems and Software in
Propositional Logic",
pages = "31--36",
note = "See also Swedish Patent {$467 076$}
and United States Patent {$5,276,897$}"}
@PROCEEDINGS{safecomp90,
editor = "B. K. Daniels",
booktitle = "Safety of Computer Control Systems, 1990
(SAFECOMP '90)",
address = "Gatwick, UK",
date = "30 Oct -- 2 Nov 1990",
publisher = "Pergamon Press",
year = 1990}
@INPROCEEDINGS{uribe-stickel,
author = "Tom{\'a}s Uribe and Mark E. Stickel",
title = "{O}rdered {B}inary {D}ecision {D}iagrams and the
{D}avis-{P}utnam Procedure",
booktitle = "{$1^{st}$} International Conference on Constraints
in Computational Logics",
editor = "Jean-Paul Jouannaud",
date = "7--9 Sep",
address = "Munich",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
volume = 845,
year = 1994,
pages = "34--49"}