Here is what I 'know' about the effectiveness of different
proof search methods for propositional logic.
Classical tableaux =/= Truth tables
| |
| |
v v
BDDs =/= d'Agostino's tableaux
| |
| |
? |
| |
| v
--------> Stalmarck
According to a paper of d'Agostino Classical tableaux and Truth tables
do not polynomially simulate each other. He proposes a minor improvement
of classical tableaux, which polynomially simulates both classical
tableaux and truth tables. BDDs are polynomially incomparable with
d'Agostino's tableaux. Examples are (phi & p) &~p with phi an arbitrary
formula with a large BDD (such formulas exist). This formula is
easy for a tableaux system (to prove a contradiction) as it ignores
phi, whereas any BDD system will construct a BDD for phi.
The Urquhart formula p1<->p2<->...<->p_n<->p1<->...<->p_n with brackets
associating to the right is a tautology. The BDD proof of this formula
is short as any intermediate BDD has size O(n). A d'Agostino proof
for this formula must be exponential in n (I am currently writing
down a proof of this). The system that Gunnar Stalmarck has proposed
is an extension of d'Agostino's tableaux. However, this is a system
that is not well defined; the few descriptions that have appeared in
print differ from the description that Gunnar Stalmarck gives when
you talk to him. However, the example above showing that BDDs behave
badly compared to d'Agostino's system also shows that BDDs
are exponentially worse than Stalmarck's system. The example
that shows that the reverse, can be handled efficiently by
Stalmarck !. So, it is possible that Stalmarck is (polynomially)
better than BDDs. This is a challenging question, because both
BDDs and Stalmarck's system have been applied for serious
applications of different kinds (correctness of a back flushing
system of a Nuclear Power plant in Sweden).
My own experience with BDDs and Stalmarck's system actually shows
that BDDs do not get me anywhere. I tried to prove safety requirements
for a railway safety unit. An somewhat ad hoc improvement of BDD
techniques, using hiding functions, allowed me to prove the correctness
of requirements in about one hour (plain BDDs filled more than 256 MB of
memory in a few minutes, failing to provide any result) and Stalmarck's
system only took 30 seconds. This very strongly contrasts with
those enthousiastic rumours that I have heard about BDDs.
I also tried to prove 3-SAT formulas with a relative high number of
different variables, and I had to conclude that BDDs are not suited for
that (in such domains several OR techniques appear outstanding).
Having had these and other experiences I was quite puzzled by the difference
in performance of different proof systems. In particular
I found it astonishing that in a field as old as automatic theorem
proving no theoretical investigation has been carried out on
something as fundamental as propositional logic. Of course many
benchmarks have been carried out, but as we all know this only gives
some impressions and hardly fundamental insight.
I think it is now time to try to make a neat classification. One of
my own plans is to try to contribute to this in the coming years
(or even better find the articles of the person who has already done
so). I am quite convinced that such a fundamental activity will
contribute highly to the effectiveness of all kinds of
automatic theorem provers.
Below I provide a number of references that people may find interesting
(forgive me for putting a few of myself among them)
J.F. Groote, J.W.C. Koorn and S.F.M. van Vlijmen. The safety
guaranteeing system at station Hoorn-Kersenboogerd.
Preprint no 121, logic group preprint series, department of
philosophy, Utrecht University, 1994. (http:\\www.phil.ruu.nl).
Extended abstract to appear in proceedings of COMPASS95).
J.F. Groote. Hiding propositional constants in BDDs.
Preprint no 120, logic group preprint series, department of
philosophy, Utrecht University, 1994. (http:\\www.phil.ruu.nl)
G. Stalmark and M. Saflund. Modelling and verifying systems and software
in propositional logic. In proceedings of SAFECOMP '90, pages 31-36.
Pergamon Press, 1990.
A. Urquhart. Complexity of proofs in classical propositional logic.
In Logic from Computer Science, ed. Y. Moschovakis Springer-Verlag.
pp. 596-608, 1992.
M.D. d'Agostino. Are tableaux an improvement on truth tables ?
Journal of Logic, Language and Information, 1, 235-252, 1992.
M.D. d'Agostino, M. Mondadori. The taming of the Cut. Classical
refutations with analytic cut. Journal of Logic and Computation.
Vol. 4. No. 3, pp. 285-319,1994.