Optimizations in Decision Procedures for Propositional Linear Inequalities

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 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 23, 2002
Accession Number
ADA461194

Entities

People

  • Ofer Strichman

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Availability
  • Classification
  • Coding
  • Computers
  • Construction
  • Contracts
  • Inequalities
  • Information Operations
  • Instructions
  • Monitoring
  • Optimization
  • Schools
  • Security
  • Standards
  • Universities

Readers

  • Artificial Intelligence
  • Graph Algorithms and Convex Optimization.