Optimizations in Decision Procedures for Propositional Linear Inequalities
CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Pagination or Media Count:
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 formulas 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.
- Theoretical Mathematics
- Operations Research