RealPaver User's Manual
Contents
1.2. Output OutputArgument NextOutput NextOutput Output epsilon OutputArgument Mode hull union Digits Integer Style bound midpoint epsilon HYERES E EEE BE SES ESS SERRES EE SEE Consistency techniques PRESSE i a STS Saas SO SRS N IC a re Consistency ConsistencyArgument NextConsistency 31 NextConsistency Consistency epsilon ConsistencyArgument local bc3 bc3_newton bc4 strong 3b weak3b phi Number width Number improve Number epsilon Split SplitArgument NextSplit NextSplit won Split epsilon SplitArgument none precision Number choice rr 1f mn parts Integer number 00 Integer mode paving points epsilon Definition of constants Constants Constant NextConstants NextConstants Constants epsilon 32 bc5 hc3 hc4 hc4T hc4_newton Constant Identifier Expr ConstName Expr Expr Vr a a a a n Definition of variables Ve a oaia oii a ao am Variables OneVariable NextVariables NextVariables Variables epsilon OneVariable VarType Identifier VariableArray in BracketBound ExpBound ExprBound BracketBound VariableArray Integer Mu Integer epsilon VarType int real
3. 904 Consistency strong 3B Variables x in 0 2 y in 0 2 Constraints y x2 3 y 2 x2 The result is just the expected box 000 OUTER BOX x in 0 9999999999999997 1 y in 0 9999999999999996 1 The splitting process of 3B consistency iteratively reduces each facet of a box In Fig 6 the 20 reduced facet corresponds to the left bound of x The width w of the domain of x in the rejected box can be parameterized The default value is set to 1073 A small value of w leads to a slow consistency algorithm that computes a tight box In RealPaver there is another strong consistency technique that we call weak 3B consistency It is stronger than local consistencies but weaker than 3B consistency Only one reduction of each facet is performed In practice should we use a local or a strong consistency technique In general implementing a local consistency is efficient This is the default mode of RealPaver If the resolution is too long one may try another technique see Section 3 5 There are also some situations where the user aims at computing only one box enclosing the solution set A first method is to use the hull option of RealPaver A second method consists in disabling the splitting process and using a strong consistency For example consider Reimer s system with 3 variables This problem is difficult Constraint solvers are sensitive to the width of the initial box 99 Variables x 1 3 in 100 100
4. Constraints x 1 72 x 2 2 x 3 2 0 5 x 1 3 x 2 73 x 3 3 0 5 x 1 4 x 2 4 x 3 4 0 5 RealPaver computes 3 boxes at 107 in 18 630ms If weak 3B consistency is applied only 2 boxes are computed in 14 670ms 000 OUTER BOX 1 x 1 in 0 3082486435333776 0 308248643533384 x 2 in 0 6353521306033765 0 6353521306033828 x 3 in 0 8992525249461816 0 8992525249461838 precision 6 49e 15 elapsed time 8 710 ms OUTER BOX 2 x 1 in 0 8992525249461806 0 8992525249461845 x 2 in 0 6353521306033739 0 6353521306033856 x 3 in 0 3082486435333729 0 308248643533387 precision 1 42e 14 elapsed time 8 730 ms END OF SOLVING Property reliable process no solution is lost Elapsed time 14 670 ms Interval Newton Given a box the interval Newton method approximates a square system of equations with func tions from C by a first order Taylor expansion around the center of the box A preconditionning of the computed linear relaxation performs a linear combination of the rows of the system which 21 may be very efficient Combining the interval Newton method with consistency techniques leads to powerful solvers The following system is hard for local consistency techniques x 2y 0 x 2y 0 x y 11 We observe the same behaviour for the aforementioned problem of the intersection of parabolas The reduction that is computed by a local consistency technique is weak if the splitting proc
5. Pom TIFF min f f max f f f natural Iff Number Constant Variable sart f log f exp cos f sin f tan f acos f asin f atan f cosh f sinh f tanh f acosh f asinh f atanh f 3 2 Branch and Prune Algorithms The constraint solving engine of RealPaver implements a branch and prune algorithm Given a CSP a set of boxes that contains all the solutions of the CSP is computed Each box is reduced and then split The reduction eliminates inconsistent values from domains by means of consistency techniques see Section 3 4 The splitting step generates sub boxes in order to separate the solutions Example Intersection of Circles Fig 2 illustrates a branch and prune computation over the aforementioned problem of intersec tion of circles The initial box is 0 6 x 3 3 box 1 initial box bisection Figure 2 Branch and Prune Computation 11 First a reduction technique may remove the hashed surface of the box The new box is 0 3 x 3 3 Suppose that no more reduction is possible this depends on reduction techniques Second the domain of y can be bisected into two parts Two sub boxes are generated 0 3 x 3 0 box 2 and 0 3 x 0 3 box 3 Then each sub box is reduced and so on The result is the union of both small gray boxes Note that a box is bisected only if it is too large with respect to a desired pr
6. 8 26 Index 3B consistency 20 arc consistency 17 bisection 11 bound consistency 18 box 6 box consistency 18 branch and prune algorithm 11 combination 21 consistency technique 5 local 17 strong 19 weakness 23 consistent value 5 constant 8 predefined 8 constraint 5 6 disjunction 11 Grammar 11 Constraint Programming 5 continuum of solutions 12 CSP 5 discrete solution set 12 domain 5 6 expression 8 9 11 feasible solution 5 hull consistency 18 hull of boxes 16 IEEE floating point number 5 9 ill conditionned 23 improvement factor 18 inconsistent value 5 infinities 9 integer constraints 9 interval 5 Interval Newton 21 largest first 13 linear relaxation 21 minimum 11 model 5 paving 12 preconditionning 21 Programming consistency 23 output 16 search 13 reduction 5 reliability 7 round robin 13 rounding error 9 safe box 22 satisfiability 7 search 5 solver 5 splitting 11 Strategy 23 type 9 union of boxes 16 variable 5 6 array 9 domain 5 hidden 9 integer 9 real 9 weak 3B consistency 21 References 10 11 12 13 14 15 16 17 18 Fr d ric Benhamou Fr d ric Goualard Laurent Granvilliers and Jean Fran ois Puget Revising Hull and Box Consistency In Procs ICLP 99 1999 Fr d ric Benhamou David McAllester and Pascal Van Hentenryck CLP Intervals R
7. find all the points x y such that x is an integer in 5 7 d is the distance between x y and xo yo and either y lt 0 or y gt x The disjunction of constraints y 0 or y gt x is implemented by the minimum operation Rewrite it as y lt 0v z ys lt 0 In other words at least one of both expressions must be negative i e their minimum must be negative The corresponding constraint is min y x y lt 0 The complete program follows 904 Constants d 1 25 5 x0 1 5 yO 0 5 Variables int x in 5 7 x is an integer variable real y in oo tool y is a real variable default type Constraints d 2 x x0 2 y y0 2 distance between x y and x0 y0 min y x y lt 0 E y lt 0 or y gt x For this problem RealPaver computes three boxes O OUTER BOX 1 x 2 y in 0 6456439237389602 0 64564392373896 precision 2 22e 16 elapsed time O ms OUTER BOX 2 xod y in 1 64564392373896 1 64564392373896 precision 2 22e 16 elapsed time O ms OUTER BOX 3 x 1 y in 0 6456439237389602 0 64564392373896 precision 2 22e 16 elapsed time O ms END OF SOLVING Property reliable process no solution is lost Elapsed time O ms 10 Grammar of Constraints A constraint is a nonlinear equation or inequation involving numbers constants variables and function symbols The complete grammar is as follows Constraint f f f gt f f lt f
8. Given a particular set of constants the complete program follows 904 Constants x0 2 yO 1 center of the given circle r 1 25 radius d 2 75 distance to origin Variables x in oo tool definition of variables y in oo tool and domains the set R Constraints r 2 x x0 72 y y0 72 the point x y is on the circle d 2 x 2 y 2 the distance from the origin is d The output is 000 OUTER BOX 1 x in 2 75 2 75 y in 2 119516683375301e 16 0 precision 4 44e 16 elapsed time 0 ms OUTER BOX 2 x in 1 649999999999999 1 650000000000001 y in 2 199999999999999 2 200000000000001 precision 2 44e 15 elapsed time 10 ms END OF SOLVING Property reliable process no solution is lost Elapsed time 10 ms The interpretation of the result is the following e The solving process is reliable this is the essential property of RealPaver Prop 1 which guarantees that the union of all the computed boxes contain all the solutions of the CSP e An outer box is a box which may contain some solutions of the CSP Here the result is the union of two boxes each solution being contained in one box Suppose now that for another set of constants the CSP has no solution for instance given zo yo 1 r 10 and d 1 What is the result In this case RealPaver guarantees that the problem has no solution 000 END OF SOLVING Property no solution in
9. are discussed in Section 3 5 3 3 Output of RealPaver The output of RealPaver can be parameterized by means of optional flags in programs as follows 99 Output digits n natural number mode union hull y style bound midpoint The first option corresponds to the number of digits for printing interval bounds The default value is set to 16 The union mode specifies that the result is presented as the list of all computed boxes The hull mode is such that the result is presented as the hull of all computed boxes i e the smallest box containing all computed boxes The bound style is such that every interval domain a b is written a b In the midpoint mode it is written m e e where m is the center of a b and e is the distance from the center to each bound For instance let us add the following lines in the program modeling the intersection of circles 16 99 Output digits 32 A mode hull style midpoint The result follows 000 OUTER BOX HULL of 2 boxes x 2 1999999999999992894572642398998 0 55 0 55 y 1 1000000000000000888178419700125 1 1 1 1 precision 2 44e 15 elapsed time 10 ms END OF SOLVING Property reliable process no solution is lost Elapsed time O ms 3 4 Consistency Techniques precise descrition of consistency techniques is out of scope of this manual However one may give the user some ideas of the capabilities of the different algorithms implement
10. language each one being prefixed by the symbol as shown in this table constant value constant value constant value constant value pi 2_pi 27 3_pi IT 4_pi Ar pi_2 03pi2 107 pi2 Qinv pi sqrt2 v2 Clog2 log 2 Variables and Domains RealPaver is able to represent two types of variables integer and real variables The default type is real However a type may be specified at the declaration as follows 904 Variables real X ID Onn y integer n in There is no specific solver for integer variables and constraints in RealPaver There is just an additionnal constraint for each integer variable that allows one to reduce the domain bounds to integer values as soon as possible Note that RealPaver is necessarily slower for integer constraints than specific solvers As for constants each domain bound can be defined by a constant expression 99 Variables x in 1 1 1 log2 The result below shows that each expression is evaluated by interval computations using the outward rounding mode of floating point computations The left bound corresponds to an evaluation of 1 1 rounded towards oo while the right bound corresponds to an evaluation of 1 log 2 rounded towards 00 As a consequence RealPaver guarantees that the input domain the one in the user s mind is included in the computed domain 000 x in 1 0999999999999998667732370449812 1 6931471805599453972490664455108 In the IEEE stand
11. of 107 we immediately obtain a small reduction 000 OUTER BOX 1 x 1 in 10 10 x 2 in 10 6 x 3 in 6 10 Elapsed time O ms If 3B consistency is used given a width of 10 the reduction is better but the solving is longer 24 009 OUTER BOX x 1 in x 2 in x 3 in Elapsed 1 9 989989979949861 0 01001002005014042 9 989989979949861 0 01001002005014042 1 580680000001182 10 time 2 010 ms If 3B consistency is used given a width of 1074 the solving process becomes much longer and the reduction is quasi equivalent 009 OUTER BOX x 1 in x 2 in x 3 in Elapsed In this case 3B 1 9 989989979949861 0 01001002005014042 9 989989979949861 0 01001002005014042 1 580936000015381 10 time 20 520 ms consistency given a width of 107 seems to be a good choice Let us try to compute a paving in the hull mode The result follows 000 OUTER BOX x 1 in x 2 in x 3 in Elapsed HULL of 1024 boxes 9 989989979949861 0 01001002005014042 9 989989979949861 0 01001002005014042 1 372542666573572 10 time 20 ms The computed box is tight and the solving time is small However the left bound of x3 is not precise with respect to the results obtained with a strong consistency technique We may increase the number of computed boxes 1024 is the default value 000 OUTER BOX x 1 in x 2 in x 3 in Elapsed HULL of 99999 boxes 9 989989979949861
12. see 14 Four kinds of intervals are manipulated nr freR ri lt r lt r2 1 400 reR n xr oo r reR r lt ra co too R The notion of model used in RealPaver is quite simple a model is a constraint satisfaction problem CSP that is composed of e A set of real valued variables e g 1 En e A set of interval domains e g 1 n e A set of numerical constraints e g C1 Cm over the given set of variables The problem is to find in the initial bor 11 x x n all the consistent values with respect to all constraints 3 1 Modeling with Constraints In this section we present the basic features of RealPaver Example Intersection of Circles Consider the following problem given a real number d gt 0 and a circle with center xo yo and radius r find all the points on the circle whose distance to the origin is d As shown in Fig 1 this is a problem of intersection of circles Figure 1 Intersection of Circles In this problem we may identify the following data e 4 constants d ro yo r Depending on their values the problem has 0 1 or 2 solutions e 2 variables the coordinates x y of the point Since these variables lie a priori in IR the variable domains are defined as the set R e 2 constraints x y is required to be on the given circle i e r 2 2 y yo the distance of x y to the origin is d i e d 2 y
13. the unknowns of a problem i e the variables For instance in geometric modeling one wants to determine a point x y in R which distance to the origin is greater than 2 The corresponding mathematical formula y z y gt 2 is just what we call a constraint The problem is to find values of the variables that satisfy the constraint or more generally all the constraints of a model The point 1 2 is a feasible solution since V1 22 gt 2 This value is declared consistent with respect to the constraint In Constraint Programming the search of solutions which is done by solvers consists in elim inating inconsistent values Initially a domain is associated to each variable e the set of possible values a priori The solvers implement domain reductions by means of consistency techniques and domain splitting in order to separate the solutions Constraint programming allows the user to design models with constraints in a very natural way as the scientist does The constraint programming system is responsible for the search of solutions Numerical Constraints RealPaver is able to solve numerical constraints i e nonlinear equations or inequality con straints over the real numbers Each constraint is defined by an analytic expression f z1 24 90 where o lt gt and f R R is a function Each domain is represented by a closed interval whose bounds belong to the set of IEEE floating point numbers
14. 0 01001002005014042 9 989989979949861 0 01001002005014042 1 569623278118378 10 time 1 920 ms A number of 10 boxes is not enough Let us try 106 In this case the result is tight Note that it is very similar to the one obtained with 3B consistency 000 OUTER BOX x 1 in x 2 in x 3 in Elapsed HULL of 1000000 boxes 9 989989979949861 0 01001002005014042 9 989989979949861 0 01001002005014042 1 582747308958421 10 time 19 100 ms 25 3 6 Related Work Interval analysis has been devised by Ramon E Moore 17 Some interval methods implemented in RealPaver have been introduced by Eldon R Hansen 11 R Baker Kearfott 15 or Arnold Neumaier 18 The framework of continuous CSPs originates from the works of John G Cleary 3 and Ernest Davis 6 These ideas have been developped by many researchers such as Fr d ric Benhamou 2 Alain Colmerauer 5 Boi Faltings 7 Timothy Hickey 12 Eero Hyv nen 13 Olivier Lhomme 16 William Older and Andr Vellino 19 Jean Fran ois Puget 1 Michel Rueher 4 Maarten Van Emden 20 and Pascal Van Hentenryck 21 The main achievement was Numerica 22 developed by Pascal Van Hentenryck et al which is a modeling language for global optimization implementing interval computations and consistency techniques Many algorithms implemented in RealPaver can be found in these early works on continuous CSPs or in the author s publications 1 10 9
15. 000000153915 x 3 in 0 9999999999576185 1 000000000035721 x 4 in 0 9999999999999982 1 000000000000002 x 5 in 0 9999999999999919 1 000000000000008 precision 7 33e 10 elapsed time 180 ms END OF SOLVING Property non reliable process some solutions may be lost Elapsed time 310 ms Using the paving mode two boxes are computed near the end of the solving process since a BFS strategy is implemented 15 000 OUTER BOX 1 x 1 in 0 9999999999974312 1 000000000002585 x 2 in 0 9999999999985194 1 000000000001401 x 3 in 0 9999999999994048 1 000000000000503 x 4 in 0 9999999999999981 1 000000000000002 x 5 in 0 9999999999999946 1 000000000000007 precision 5 15e 12 elapsed time 550 ms OUTER BOX 2 x 1 in 0 9163545825330509 0 916354582534548 x 2 in 0 9163545825334893 0 9163545825341433 x 3 in 0 9163545825337194 0 9163545825339365 x 4 in 0 9163545825338468 0 9163545825338524 x 5 in 1 41822708733075 1 418227087330761 precision 1 5e 12 elapsed time 550 ms END OF SOLVING Property reliable process no solution is lost Elapsed time 550 ms Combining the paving mode with a maximum computation time of 300ms is dangerous for problems having a discrete solution set In this case a paving composed of about 140 boxes is computed though they can be efficiently reduced in about 200ms Is there an ideal strategy Should we use the paving mode or the default mode These aspects
16. 9516683375301e 16 0 precision 4 44e 16 elapsed time 0 ms END OF SOLVING Property non reliable process some solutions may be lost Elapsed time O ms Is there a difference between both problems when n 00 In both cases the result is neces sarily a paving composed of boxes at the desired precision Nevertheless the splitting search strategy is different e A paving must be composed of boxes that have approximatively the same precision To do so boxes are processed in Breadth First order BFS i e a First In First Out strategy for managing the list of boxes e For the second problem the aim is to compute boxes at the given precision as fast as possible Then boxes are processed in Depth First order DFS i e a Last In First Out strategy Programming the Search Optional flags can be added in programs The first possible action is to disconnect the splitting process In this case only a reduction phase is performed 99 Split none Otherwise if the splitting process is enabled several components of the strategy can be param eterized Split choice rr 1f mn 5 parts 2 3 gt precision p real number mode paving points number n 00 natural number or 00 There are 3 choice strategies of bisected domains implemented in the system e rr or round_robin the variables are chosen according to a lexicographic order fixed a priori This is the default value e 1f or largest
17. 996337671 1 000000000366426 x 2 in 0 9999999998326983 1 000000000153915 x 3 in 0 9999999999576185 1 000000000035721 x 4 in 0 9999999999999982 1 000000000000002 x 5 in 0 9999999999999919 1 000000000000008 precision 7 33e 10 elapsed time 180 ms 14 000 OUTER BOX 2 x 1 in 0 9163545825338459 0 9163545825338514 x 2 in 0 9163545825338464 0 9163545825338519 x 3 in 0 9163545825338466 0 9163545825338516 x 4 in 0 9163545825338462 0 9163545825338518 x 5 in 1 418227087330746 1 418227087330764 precision 1 82e 14 elapsed time 460 ms END OF SOLVING Property reliable process no solution is lost Elapsed time 580 ms If the output is required to be the hull of the computed boxes see Sec 3 3 we obtain only one box at the end of the splitting process 000 OUTER BOX HULL of 2 boxes x 1 in 0 9163545825338459 1 000000000366426 x 2 in 0 9163545825338464 1 000000000153915 x 3 in 0 9163545825338466 1 000000000035721 x 4 in 0 9163545825338462 1 000000000000002 x 5 in 0 9999999999999919 1 418227087330764 precision 0 976 elapsed time 570 ms END OF SOLVING Property reliable process no solution is lost Elapsed time 570 ms If an upper bound for the computation time is set to 300ms only one box is computed and the property of reliability is no more guaranteed O OUTER BOX 1 x 1 in 0 9999999996337671 1 000000000366426 x 2 in 0 9999999998326983 1 000
18. DAMAGE 2 Installation Software and Hardware Requirements The compilation of RealPaver requires a recent ANSI C compiler e g gcc 2 95 2 and GNU make To date RealPaver is known to compile on ix86 computers under Linux Sun Sparc computers under Solaris 2 5 and SGI computers under IRIX 6 5 Installation The installation of RealPaver is done in three steps 1 Put the tarball in a directory where you have write permissions and unpack it gzip c d realpaver 0 4 tar gz tar xf 2 Enter the subdirectory and configure RealPaver cd realpaver 0 4 configure 3 Build RealPaver gmake The profiling mode of RealPaver can be enabled at configuration time as follows configure enable profile Use of RealPaver You should be able to call RealPaver on a file filename by the following command realpaver filename The on line help is obtained with realpaver h Bug Report Please report bugs to Laurent Granvilliers by e mail or by regular mail with subject RealPaver bug Suggestions for improvement are most welcome LINA Facult des Sciences 2 rue de la Houssiniere B P 92208 44322 Nantes Cedex 3 France Laurent Granvilliers lina univ nantes fr 3 Overview RealPaver is a modeling language for numerical constraint solving In this section we will describe how problems are modeled using RealPaver and how models are solved Constraint Programming A constraint is a relation between
19. Intersection of Circles Constants 2d wor ach koe pied RO a 4A BOX x 3 WA E de Variables and Domains s lt ia s e wu a nie m XR m RR RAE a A Example Disjunctive Constraints Grammar of Vonsiramis loli loe ow dat e Re ae 3 2 Branch and Prune Algorithms Example Intersection of Circles 4 4 ce Lu e nun db rara ae Paving or NOt oo coc basin aie A a de dd vor ob he a dur Progranimiug the Search c a su san am e Ro bos de Roe Ae ee a d Example Brown s problem 33 Output of RealPaver gt c 2 222 2 84246 o a 8 Ro RR 3S E OX 9 de 24 Consisteney Techniques occorra 25 be kde sn eA dose RUE ar a a Example ele oo de da aaa D Ad er dual l Strong Consisteney Techmauss e so 4 VOY cel Ei 9x 3 Lib ral MENTON di ui dus ue 3 e Pa e Bon Up R a EU E DR eu Programming with Consistency Techniques 3 5 Programming the Strategy uoce ee eA Xy S EROR E cn a ee 20 Related Work u u uo oos ORE a Pa RR as hu aa Index References Grammar of the Language 111 He 1 Distribution RealPaver 0 4 BSD License Copyright c 1999 2003 Institut de Recherche en Informatique de Nantes IRIN France Copyright c 2004 Laboratoire d Informatique de Nantes Atlantique LINA France All rights reserved The following terms apply to all files associated with th
20. RealPaver User s Manual Solving Nonlinear Constraints by Interval Computations Edition 0 4 for RealPaver Version 0 4 August 2004 Laurent Granvilliers Copyright 1999 2003 Institut de Recherche en Informatique de Nantes France Copyright 2004 Laboratoire d Informatique de Nantes Atlantique France Laurent Granvilliers Laboratoire d Informatique de Nantes Atlantique Universit de Nantes B P 92208 F 44322 Nantes cedex 3 France Laurent Granvilliers univ nantes fr The authors hereby grant you non exclusive and non transferable license to use copy and modify this manual for non commercial purposes Acknowledgements I would like to thank Fr d ric Benhamou and Fr d ric Goualard for many interesting discussions on interval constraint satisfaction techniques and Luc Jaulin who gave me interesting feedback on an early version of RealPaver Tam grateful to the members of the Constraint Programming Group at the University of Nantes for their encouragement Many thanks to Martine Ceberio who was an incorruptible beta tester Contents 1 Distribution Ino TT 2 Installation Software and Hardware Requirements Installation D De LA ee ee me 4 She A Ge a Dee or RealPayer CC c Bug Report 2e Xon SARS a eani A SNS RE Ee DES 3 Overview Constraint PTOBDGUGEDM cs x vcio ee A u eg Numerical Vonsiraitis os 12 xor Roo Ro a 3 1 Modeling with Constraints Example
21. arch Continuous Problems Kluwer Dordrecht The Netherlands 1996 Olivier Lhomme Consistency Techniques for Numeric CSPs In Procs IJCAI 93 1993 Ramon E Moore Interval Analysis Prentice Hall Englewood Cliffs NJ 1966 Arnold Neumaier Interval Methods for Systems of Equations Cambridge University Press 1990 29 19 William Older and Andr Vellino Constraint Arithmetic on Real Intervals In F Benhamou and Colmerauer editors Constraint Logic Programming Selected Research MIT Press 1993 20 Maarten H Van Emden Value Constraints in the CLP Scheme Constraints 2 2 163 183 1997 21 Pascal Van Hentenryck David McAllester and Deepak Kapur Solving Polynomial Systems Using a Branch and Prune Approach SIAM Journal on Numerical Analysis 34 2 797 827 1997 22 Pascal Van Hentenryck Laurent Michel and Yves Deville Numerica a Modeling Language for Global Optimization MIT Press 1997 30 Grammar of the Language A program is a list of pragmas First Pragma NextPragma NextPragma First epsilon Pragma Constants Constants Variables Variables Constraints Constraints Consistency Consistency Split Split Output Output Time Number Y JR 9 Management of output
22. ard the infinities are completely specified so as to define infinite projective values for the set of floating point numbers Their use as interval bounds is allowed in RealPaver However note that rounding errors are non negligible near the infinities and it may be difficult to remove these values from domains Should we use the infinities or not Yes but only if no more information is known about the variables For instance given a variable that represents a distance between two places on Earth the domain 0 5e4 is preferred to R since 5e4 is an upper bound of Earth s circumference In many situations the definition of arrays of variables is required This is done as follows 904 Variables x 1 3 in 1 1 This just declares 3 different variables x 1 x 2 x 3 having the same initial domain Finally there is often a motivation to share complex expressions between constraints This can be done by using a new variable lying in R defining a new equation between the variable and the expression and replacing the expression by the variable in the constraints However the value of this variable has generally no sense for the user In RealPaver there exists a mechanism for hidding such variables just adding the symbol in the definition of the variable as follows 904 Variables z in l oo tool hidden variable Example Disjunctive Constraints A second problem is considered now given a point ro yo and a real d gt 0
23. called constraint propagation can be parameterized by an improvement factor q interpreted as follows if the width of a domain is reduced by a factor less than q then it is declared unchanged If all domains are declared unchanged then the propagation terminates 18 The factor q 0 corresponds to the tightest algorithm How may q be tuned For example consider the following program that has no solution 904 Consistency improve 0 improvement factor Variables x 1 2 in 1 1 Constraints x 2 x 1 A x 2 x 1 1 0e 5 The result follows RealPaver detects the unsatisfiability in half a second using a factor of 0 The solving time is rather long since this problem is ill conditionned 000 END OF SOLVING Property no solution in the initial box Elapsed time 500 ms In this case the reduction must be as tight as possible in order to limit the combinatorial explosion of search algorithms For example let us try another value q 30 The computation time is much greater 000 END OF SOLVING Property no solution in the initial box Elapsed time 1 080 ms Finally a factor of q 50 leads to the generation of 144 boxes with a precision of 1078 in 1600ms 000 END OF SOLVING Property reliable process no solution is lost Elapsed time 1 600 ms However in practice it is often desired to slightly weaken the propagation process To this end the default value of the improvement factor is 10 Strong Consisten
24. cy Techniques The aforementionned consistency techniques are said to be local In particular each reduction is applied over one domain with respect to one constraint Such an approach may be weak For example consider the intersection of two parabolas see Fig 5 The aim is to compute a tight box enclosing the solution However the initial box cannot be reduced while removing solutions of c Moreover it cannot be reduced while removing solutions of co As a consequence it cannot be reduced The problem is that the conjunction of constraints is not taken as a whole The locality problem is handled by strong consistency techniques Roughly speaking local con sistency techniques are just combined with a search algorithm For the problem of intersection 19 solution Figure 5 Conjunction of Constraints of parabolas the domain of x is first bisected see Fig 6 Zi C1 ea y w Figure 6 Strong Consistency Then the left hand box is rejected it is first reduced with respect to c1 and the resulting topmost gray box contains no solution of ca Moreover the right hand box is reduced the topmost hashed box contains no solution of c and the bottommost hashed box contains no solution of ca An iteration of such a splitting step permits the computation of a tight box around the solution The complete program follows RealPaver implements the so called 3B consistency technique
25. ecision fixed a priori The precision of a box is the maximum precision componentwise and the precision of an interval a b is the quantity b a Paving or Not RealPaver is able to tackle the following problems given a natural n 1 Compute at most n boxes that contain all the solutions of the CSP 2 Compute at most n boxes at the desired precision The first problem deals with the computation of a paving of the solution space This mode is useful for representing continui of solutions by a finite number of boxes The maximum number of boxes n is a parameter The following figure illustrates a paving of 10 boxes for the constraint y x 0 8 on the box 1 1 The hashed surface represents the set of solutions N N N K 1 Figure 3 Paving of a continuous set of solutions Note that the number of boxes in the paving is also bounded by the number of boxes of the desired precision that are contained in the initial box since the sufficiently tight boxes are not bisected The second problem deals with the computation of boxes at the desired precision This is typically used for representing discrete sets of solutions Note that such a process may not be reliable since some solutions may be lost due to the maximum number of computed boxes fixed a priori For instance for the problem of intersection of circles if this number is 1 RealPaver returns one box 12 000 OUTER BOX 1 x in 2 75 2 75 y in 2 11
26. ed in RealPaver A consistency property determines which values from domains are consistent or not with respect to the constraints of a CSP If the property is reliable the inconsistent values do not partic ipate in any solution Given a consistency property a consistency or reduction technique just eliminates some inconsistent values from domains Example Circle Consider a circle defined by x y 2 and the box 2 4 x 1 1 The solution space is the infinite set of points on the circle that belong to the box see Fig 4 Figure 4 Solution Space and Consistency On the one hand the domain of y cannot be reduced since all the values in 1 1 are consistent i e these values participate in a solution On the other hand the domain of x can be reduced 2 V2 U 1 1 U V2 4 is the set of inconsistent values In Fig 4 the hashed surfaces represent the corresponding sub boxes 17 Removing all the inconsistent values from the domain of x can be done by the arc consistency technique However this is not reachable over the floating point numbers since y2 is not exactly represented Moreover it is often more efficient to reduce domains at bounds i e to keep interval domains This is done by bound consistency techniques The approximation of bound consistency over interval domains is called hull consistency and it is implemented in RealPaver HC3 and HC4 algorithms A reduction step over this proble
27. epsilon BracketBound epsilon ExprBound pred succ epsilon Expr Definition of constraints Constraints Constraint NextConstraints 33 NextConstraints Constraints epsilon Constraint obs Identifier epsilon Expr Relation Expr Relation E lt gt in A Aia i m SERRE SE RER a HE TE DEE HE IE Definition of expressions Ci caca ca aa a an R co ca Expr Expr ExprMul Expr ExprMul ExprMul ExprMul ExprMul ExprExp ExprMul ExprExp ExprUnit Exposant Exposant xx Identifier Integer epsilon ExprUnit Expr Identifier Number ExprMul ExprMul sqrt Expr exp Expr log Expr min n Expr M Expr ny max Expr Expr cos Expr sin Expr Lan Expr cosh Expr sinh Expr tanh Expr 34 acos Expr as in n Expr at an Expr acosh Expr asinh Expr at anh Expr Identifier a zA Z a zA Z0 9_ IdentArray IdentArray Integer epsilon Number Integer Float 00 o00 Float 0 9 0 9 0 9 0 9 E Wen cram ng epsilon 0 9 Integer 0 9 39
28. ess is disabled 000 OUTER BOX x in 1 1 y in 0 5 0 5 precision 2 elapsed time O ms The combination of local consistency techniques with the interval Newton method that is imple mented by Algorithm BC5 is efficient This is the default mode of RealPaver where the interval Newton method is used only if a square system of equations can be extracted from the CSP 000 OUTER BOX x 0 y 0 In some cases a box is declared to be safe 1 e it certainly contains only one solution For instance let us solve the following problem with BC5 99 Variables x 1 2 in 1 1 Constraints x 1 72 x 2 A x 1 2 x 2 2 2 The result follows 000 SAFE OUTER BOX 1 x 1 1 x 2 1 SAFE OUTER BOX 2 x 1 1 x 2 1 22 Programming with Consistency Techniques In practice several decisions have to be taken local or strong consistency Which technique What values for the improvement factor and the splitting parameter w of strong consistencies All these methods can be compared with respect to their tightness Roughly speaking hull consistency is weaker than box consistency etc hc3 hc4 bc3 bc4 lt bed lt weak3B lt 3B m hull box hull box hull box Newton But the weaker the faster Many local consistency algorithms are implemented in RealPaver There are two reasons that allows experts in constraint programming to compare the different techniques and the best ave
29. evis ited In Procs ILPS 94 1994 John G Cleary Logical Arithmetic Future Computing Systems 2 2 125 149 1987 H l ne Collavizza Fran ois Delobel and Michel Rueher Comparing Partial Consistencies Reliable Computing 5 3 213 228 1999 Alain Colmerauer Prolog IV Specifications Esprit project 5246 1995 Ernest Davis Constraint Propagation with Interval Labels Artificial Intelligence 32 281 331 1987 Boi Faltings Arc Consistency for Continuous Variables Artificial Intelligence 65 2 363 376 1994 Laurent Granvilliers On the Combination of Interval Constraint Solvers Reliab Comput 7 6 467 483 2001 Laurent Granvilliers and Fr d ric Benhamou Progress in the Solving of a Circuit Design Problem J Global Optim 20 2 155 168 2001 Laurent Granvilliers Fr d ric Goualard and Fr d ric Benhamou Box Consistency through Weak Box Consistency In Procs IEEE ICTAI 99 1999 Eldon R Hansen Global Optimization using Interval Analysis Marcel Dekker 1992 Timothy J Hickey Metalevel interval arithmetic and verifiable constraint solving Journal of Functional and Logic Programming 2001 7 2001 Eero Hyv nen Constraint Reasoning based on Interval Arithmetic The Tolerance Propa gation Approach Artificial Intelligence 58 71 112 1992 IEEE IEEE Standard for Binary Floating Point Arithmetic Technical Report IEEE Std 754 1985 1985 Reaffirmed 1990 R Baker Kearfott Rigourous Global Se
30. first the variable whose domain is the largest one the less precise is chosen e mn or max narrow the variable associated to the maximum absolute column sum norm 13 of the Jacobian matrix is chosen If the Jacobian matrix cannot be computed then the round robin strategy is used The parts option defines the number of sub boxes generated at each splitting step Only subdivisions in 2 or 3 parts are currently supported The precision option corresponds to the precision under which boxes are not bisected The default value is set to 1078 The two last options mode and number permit implementing the two problems handled by RealPaver computation of a paving or not In the paving mode the choice strategy is necessarily largest first Note that the default mode is points not paving and the default number of computed boxes is 1024 Finally it is also possible to stop the search if the computation is too long It suffices to add the following flag in programs 99 Time t maximum computation time in milliseconds Note that this option may invalidate Property 1 if the resolution is prematurely stopped then some solutions may be lost Example Brown s problem Brown s system is a square quasi linear system of n equations n 1 ul j L n 1 1 M t zi 2 2 1 n For n 5 RealPaver with the default mode generates two boxes there are 2 solutions 000 OUTER BOX 1 x 1 in 0 9999999
31. is software that are mentionned in the file manifest txt Redistribution and use in source and binary forms with or without modification are permitted provided that the following conditions are met e Redistributions of source code must retain the above copyright notice this list of conditions and the following disclaimer e Redistributions in binary form must reproduce the above copyright notice this list of con ditions and the following disclaimer in the documentation and or other materials provided with the distribution e Neither the name of the LINA nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBU TORS AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FIT NESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT INDIRECT INCIDENTAL SPECIAL EXEMPLARY OR CONSEQUENTIAL DAMAGES INCLUD ING BUT NOT LIMITED TO PROCUREMENT OF SUBSTITUTE GOODS OR SER VICES LOSS OF USE DATA OR PROFITS OR BUSINESS INTERRUPTION HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY WHETHER IN CONTRACT STRICT LIABILITY OR TORT INCLUDING NEGLIGENCE OR OTHERWISE ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
32. m computes the following box 000 OUTER BOX x in 1 414213562373095 1 414213562373095 y in 1 1 For this constraint hull consistency is perfect no more reduction at domain bounds is possible while preserving the solution set However it is very sensitive to the multiple occurrences of variables For instance rewrite the equation as x x x y 2 In this case RealPaver with hull consistency does not reduce the initial box 0009 OUTER BOX x in 2 4 y in 1 1 This problem is handled by box consistency which is also implemented in RealPaver BC3 algorithm For the circle problem with z x x y 2 box consistency is perfect as shown below 000 OUTER BOX x in 1 414213562373095 1 414213562373095 y in 1 1 The implementation of box consistency is just a search process over z that removes the incon sistent values from its bounds The depth of the search can be parameterized by the width y of boxes that are examined y 0 is the best precision For instance the computation for p 0 05 is the following The resulting box is larger but the computation is faster 000 OUTER BOX x in 1 453703703703703 1 415020576131686 y in 1 1 In practice the combination of hull consistency and box consistency is efficient This is auto matically done in RealPaver by Algorithm BCA Given a set of constraints the domain reductions are iterated until no domain can be sufficiently reduced This process
33. rage method in precision and time for each problem is dynamically chosen by the hard coded strategy The following piece of code may be added in programs 000 Consistency local hc3 hc4 hull consistency hc4_newton hull consistency interval Newton bc3 box consistency bc3_newton box consistency interval Newton bc4 hull consistency box consistency bc5 hull box consistency interval Newton phi value precision of box consistency improve n improvement factor for local consistencies strong weak3B 3B weak 3B and 3B consistency width w splitting factor for strong consistencies 3 5 Programming the Strategy The default solving strategy of RealPaver applies a local consistency algorithm to compute at most number boxes at the given precision the best average strategy for problems having discrete sets of solutions T he choice of the local consistency algorithm is done by the system In this mode two main problems can be encountered e Nothing happens There are two possible reasons The model is ill conditionned for example x y 2 x 1075 y 2 The current version of RealPaver fails In the future we plan to implement a symbolic module in order to preprocess such systems The local consistency technique is too weak locality problem A strong consistency like weak 3B consistency or 3B consistency may be used The
34. the initial box Elapsed time O ms Property 1 Reliability Given a CSP RealPaver computes a union of boxes that contains all the solutions of the CSP In the literature this property is often called completeness property However we believe that there may be a confusion with respect to the notion of completeness in Constraint Logic Pro gramming where a complete solver is able to decide for the satisfiability of a CSP it always answers no if the CSP has no solution and yes otherwise Actually we just use the terminology of the interval framework Property 1 has a very important corollary that allows one to detect the unsatisfiability of a CSP Corollary 1 Property 1 Given a CSP if no box is computed by RealPaver then the CSP has no solution Constants constant is a symbol defined by a numerical value or more generally a constant expression involving real numbers operations and already defined constants For instance consider the following piece of program 99 Constants a 4 R b 1 sgrt a c log 2 3 d 1 1 3 RealPaver just computes an interval for each constant Moreover it guarantees that the real number defined by the right hand expression is contained in the computed interval as follows 000 a 4 b 1 c in 0 69314718055994506418215905796387 0 69314718055994550827136890802649 d in 1 0999999999999998667732370449812 1 1000000000000000888178419700125 There are several predefined constants in the
35. tuning of the width is 23 very important If the width is too large then no reduction is computed If the width is too small then the solving time is too long We suggest to progressively decrease its value in order to detect a threshold for reductions e huge number of boxes is computed There are two possible reasons The model is ill conditionned continuum of solutions is bisected In this case the paving mode should be used In the paving mode two parameters have to be tuned the precision and the number of computed boxes However the tuning may be hard if the user has no idea of the geometry of the solution set In the future we plan to combine RealPaver with a graphical interface in order to represent pavings In many situations the aim is to compute only one box enclosing the solution set We propose two different methods e The splitting process is disabled 2 e the initial box is reduced and the algorithm termi nates In this case there is often the need for applying a strong consistency technique in order to reduce the box the most possible e The paving mode is on and the hull of all the computed boxes is returned For example consider the following program 99 Variables x 1 3 in 10 10 Constraints x 1 x 2 x 3 15 x 1 x 2 x 3 0 max x 1 x 2 x 2 x 3 lt 0 If the splitting process is disabled the initial box is not reduced If weak 3B consistency is applied given a width
Download Pdf Manuals
Related Search