CMU-CS-02-133
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-02-133

Optimizations in Decision Procedures for Propositional Linear Inequalities

Ofer Strichman

May 2002

CMU-CS-02-133.ps
CMU-CS-02-133.pdf

Keywords:Verification, decision-procedure, equality-logic, conjunctions-matrices


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 reports@cs.cmu.edu