Reducing Separation Formulas to Propositional Logic

Abstract

We show a reduction to propositional logic from a Boolean combination of inequalities of the form Vi is greater or equal Vj + C and Vi is less than Vj + C where C is a constant, and Vi, Vj are variables of type real or integer. Equalities and uninterpreted functions can be expressed in this logic as well. We discuss the advantages of using this reduction as compared to competing methods, and present experimental results that support our claims.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 16, 2003
Accession Number
ADA461197

Entities

People

  • Ofer Strichman
  • Randal Bryant
  • Sanjit A. Seshia

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Computers
  • Guidance
  • Inequalities
  • Information Operations
  • Integrals
  • New Jersey
  • Railroads
  • Simplex Method
  • Splitting
  • Standards
  • Universities
  • Verification

Readers

  • Library and Information Science/ Studies, Southeast Asia Studies, Bibliography of Vietnam and Lao Studies.
  • Mathematical Modeling and Probability Theory.
  • Regression Analysis.