Delivery-Date: 
To: qed@mcs.anl.gov
Subject: Re: QED Workshop.
In-reply-to: Your message of "Thu, 27 Apr 1995 12:52:00 PDT." <01HPU1JCKIXE00004Y@pnl.gov>
Date: Fri, 28 Apr 1995 12:04:03 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:024100:950428110413"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


Jan Friso Groote asks:

| 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"}