View Full Document

# Deciding Linear Inequalities by Computing Loop Residues

View Full Document
View Full Document

6 views

Unformatted text preview:

Deciding Linear Inequalities by Computing Loop Residues ROBERT SHOSTAK SRI International Menlo Park Cahforma ABSTRACT V R Pratt has shown that the real and integer feastbdlty of sets of linear mequallUesof the form x y c can be decided quickly by examining the loops m certain graphs Pratt s method is generahzed first to real feaslbdlty of mequahues m two variables and arbitrary coefficients and ultimately to real feaslbdlty of arbitrary sets of hnear mequahtles The method is well suited to apphcatlons m program verification KEY WORDS AND PHRASES theorem proving decision procedures program venficauon linear programmmg CRCATEGORIES 3 15 369 521 532 541 1 lntroductton Procedures for deciding w h e t h e r a given set o f linear inequalities has solutions often play a n i m p o r t a n t role in deductive systems for p r o g r a m verification A r r a y b o u n d s checks a n d tests o n index variables are b u t two o f the m a n y c o m m o n p r o g r a m m i n g constructs that give rise to formulas i n v o l v i n g inequalities A n u m b e r o f approaches have been used to decide the feasibdity of sets o f inequalities 3 8 9 16 22 r a n g i n g from g o a l d r i v e n rewriting m e c h a n i s m s 27 to the powerful simplex techniques 8 o f linear p r o g r a m m i n g Some simple m e t h o d s are well suited to the small trivial p r o b l e m s that most often arise but are insufficiently general Full scale simplex techniques o n the other h a n d are general a n d fast for m e d i u m to large problems b u t do not take a d v a n t a g e of the trivial structure o f the small p r o b l e m s revolving only a few variables a n d equations e n c o u n t e r e d most f r e q u e n t l y in p r o g r a m verification a n d related applications T h e algorithm presented here retains the generality n e e d e d i n the exceptional case w i t h o u t sacrifice o f speed a n d simplicity in the more typical small p r o b l e m case It builds o n V R Pratt s o b s e r

## Access the best Study Guides, Lecture Notes and Practice Exams Unlocking...