Accession Number:

ADA461194

Title:

Optimizations in Decision Procedures for Propositional Linear Inequalities

Descriptive Note:

Technical rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

2002-05-23

Pagination or Media Count:

11.0

Abstract:

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.

Subject Categories:

  • Theoretical Mathematics
  • Operations Research

Distribution Statement:

APPROVED FOR PUBLIC RELEASE