View Full Document

Deciding Linear Inequalities by Computing Loop Residues



View the full content.
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

Loading Unlocking...
Login

Join to view Deciding Linear Inequalities by Computing Loop Residues and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Deciding Linear Inequalities by Computing Loop Residues and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?