CMU-CS-00-110 Computer Science Department School of Computer Science, Carnegie Mellon University
Combining Decision Diagrams and SAT Procedures for Poul F. Williams*, Armin Biere**, Edmund M. Clarke, Anubhav Gupta February 2000
CMU-CS-00-110.ps
Our technique is based on a quantification procedure that allows us to eliminate quantifiers in Quantified Boolean Formulas (QBF). The basic step of this procedure is the up-one operation for BEDs. In addition we list a number of important optimizations to reduce the number of basic steps. In particular the optimization rule of quantification-by-substitution turned out to be very useful: exists x : {g /\ ( x <-> f )} = g[f/x]. The rule is used (1) during fixed point iterations, (2) for deciding whether an initial set of states is a subset of another set of states, and finally (3) for iterative squaring. 12 pages
*Department of Information Technology, Technical University of Denmark | |
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |