Several decision procedures that were published in the last few years for sub-theories of propositional linear inequalities, i.e., a Boolean combination of predicates that belong to the theory, are based on a graph-based analysis of the formula's predicates. The analysis is always based on the predicates while ignoring the Boolean connectives between them. In this note we show how taking this information into account can significantly reduce the (practical) complexity of the decision procedure.

10 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by [email protected]