Boolean Satisfiability with Transitivity Constraints

<p> </p><p>We consider a variant of the Boolean satisfiability problem where a subset E</p> <p>of the propositional variables appearing in formula F sat encode a symmetric, transitive, binary relation over N elements. Each of these <em><em>relational </em></em>variables, e, i, j, for 1, 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 ^ e 2,3 --> 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. </p> <p>To use a conventional Boolean satisfiability checker,we augment the set of clauses expressing F </p><p>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. </p><p>To use Ordered Binary Decision Diagrams (OBDDs), we show that for some sets E</p> <p></p> <p></p> <p>, 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 </p><p>sat, our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem.</p> <p></p> <p></p>