CMU-CS-00-101Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-00-101
Randal E. Bryant, Miroslav N. Velev June 2000
CMU-CS-00-101.ps
Keywords: Formal verification, Boolean satisfiability, decision
procedures
To use a conventional Boolean satisfiability checker, we augment the set of clauses expressing Fsat with clauses expressing the transitivity constraints. We consider methods to reduce the number of such clauses based on the sparse structure of the relational variables. To use Ordered Binary Decision Diagrams (OBDDs), we show that for some sets E, the OBDD representation of the transitivity constraints has exponential size for all possible variable orderings. By considering only those relational variables that occur in the OBDD representation of Fsat, our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem. 23 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |