> 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.
Though at last year's CAV meeting in Stanford (CAV is heavily automated proof
and BDD etc orientated) several people were saying that BDDs were running
out of steam with the size of problems people wanted to do (we're talking
several days CPU time on some of the biggest machines that Sun have etc)
and that they were wanting to look into theorem provers to see if that
approach could be layered on top of BDDs to give handle the sorts of
abstractions etc that are required to get BDD systems down to manageable
sizes.