Boolean Satisfiability with Transitivity Constraints

TL;DR

This paper addresses the challenge of solving Boolean satisfiability problems with embedded transitivity constraints, crucial for verifying equality logic in microprocessor verification, by exploring clause reduction and OBDD representations.

Contribution

It introduces methods to efficiently handle transitivity constraints in SAT problems, including clause reduction techniques and analysis of OBDD representations for improved solving.

Findings

Transitivity constraints can cause exponential blowup in OBDD size.

Clause reduction based on problem structure improves efficiency.

Relevant transitivity constraints can be effectively represented and solved using OBDDs.

Abstract

We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula Fsat 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 Fsat 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. 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.