Abstract
We consider a variant of the Boolean satisfiability problem where a subset \(\cal E\) of the propositional variables appearing in formula F sat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, e i,j , for 1 ≤i < j ≤N, expresses whether or not the relation holds between elements i and j. The task is to either find a satisfying assignment to F sat that also satisfies all transitivity constraints over the relational variables (e.g., \(e_{1,2} \land e_{2,3} \Rightarrow e_{1,3}\)), or to prove that no such assignment exists. Solving this satisfiability problem is the final and most difficult step in our decision procedure for a logic of equality with uninterpreted functions. This procedure forms the core of our tool for verifying pipelined microprocessors.
To use a conventional Boolean satisfiability checker, we augment the set of clauses expressing F sat 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 \(\cal 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 F sat, our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem.
This research was supported by the Semiconductor Research Corporation, Contract 99-DC-684
Chapter PDF
References
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Bryant, R.E., German, S., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 470–482. Springer, Heidelberg (1999)
Bryant, R.E., German, S., Velev, M.N.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic,Technical report CMU-CS-99-115, Carnegie Mellon University (1999), Available as http://www.cs.cmu.edu/~bryant/pubdir/cmu-cs-99-115.ps
Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints, Technical report CMU-CS-00-101, Carnegie Mellon University (2000), Available as http://www.cs.cmu.edu/~bryant/pubdir/cmu-cs-00101.ps
Burch, J.R., Dill, D.L.: Automated verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Burch, J.R.: Techniques for verifying superscalar microprocessors. In: 33rd Design Automation Conference (DAC 1996), pp. 552–557 (June 1996)
Goel, A., Sajid, K., Zhou, H., Aziz, A., Singhal, V.: BDD based procedures for a theory of equality with uninterpreted functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 244–255. Springer, Heidelberg (1998)
Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 2nd edn. Morgan-Kaufmann, San Francisco (1996)
Leighton, F.T.: Introduction to Parallel Algorithms and Architectures: Arrays, Trees, and Hypercubes. Morgan Kaufmann, San Francisco (1992)
Marques-Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)
Marques-Silva, J.P.: The impact of branching heuristics in propositional satisfiability algorithms. In: 9th Portugese Conference on Artificial Intelligence (September 1999)
Rose, D.: Triangulated graphs and the elimination process. Journal of Mathematical Analysis and Applications 32, 597–609 (1970)
Velev, M.N., Bryant, R.E.: Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 37–53. Springer, Heidelberg (1999)
Yannakakis, M.: Computing the minimum fill-in is NP-complete. SIAM Journal of Algebraic and Discrete Mathematics 2, 77–79 (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bryant, R.E., Velev, M.N. (2000). Boolean Satisfiability with Transitivity Constraints. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_10
Download citation
DOI: https://doi.org/10.1007/10722167_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive