|
|
|
|
|
|
|
|
Applying Interval Arithmetic to Real, Integer and Boolean Constraints
Appeared in Volume 6/2, May 1993
Extended abstract
Frédéric Benhamou and William J. Older
The introduction of relational arithmetic within Prolog is strongly related to the Constraint LP scheme [5, 3, 10, 1]. As is well-known, the CLP paradigm replaces the unification concept of Prolog by the notion of constraint resolution. Different algebraic structures have been examined by various CLP systems, in order to improve Prolog's expressiveness and efficiency by adding constraint solving on specific domains.
However, one of the major drawbacks of these CLP systems is the strong partitioning of the structures in which constraints can be expressed. This means that one cannot express constraints involving discrete and continuous domains, that a boolean value cannot be involved in any numerical constraint, and that it is not possible to use the boolean value associated with a numerical relation in any boolean constraint.
The aim of this paper is to show that interval arithmetic is an appropriate theoretical model for a CLP language where both expressiveness and efficiency are significantly improved by allowing the user to express constraints on reals, integers and booleans (including booleans representing numerical relations) in a unified framework.
R. Moore [7] pioneered the field by introducing functional interval arithmetic to deal with the incorrect behaviours of finite precision arithmetic. To provide a sound, relational model for numeric processing in Prolog, relational arithmetic on real intervals has been proposed by John Cleary in [2]. In his model, constraint solving is limited to interval-convex relations (relations built from continuous, monotonic functions) and involves the use of non-logical variables. W. Older and A. Vellino, in [8], discuss the implementation of such a scheme in BNR-Prolog, and propose a general theoretical framework which makes use of lattice theory to establish a fixed point semantics for the processing of interval constraint networks involving non interval-convex relations. Related work includes [6] and [9].
We first introduce the set F of F-intervals which are real intervals whose bounds are taken either in {-infinity, +infinity} or in a finite subset of R. An interesting instance of such a subset is the set of numbers exactly representable with floating points numbers. Cartesian products of F-intervals are called F-blocks. We then show how any subset of R can be approximated by an F-interval, and extend the notion of approximation by an F-block to any n-ary relation p on R. The approximation of p is denoted by approx(p). Significantly, there is no restriction to interval-convex relations. The next step consists in defining, for every n-ary relation p on R, a narrowing function, denoted by p^, which maps Fn to Fn, and such that for every F-block u,
p^(u) = approx(u /\ p).
We end the section by proving the correctness, contractance, monotonicity and idempotence of these functions.
The second section is devoted to the introduction of constraints on real numbers. These constraints are in the form p(x1,...xn), where p is a n-ary relation on R , and every xi is either a variable whose value can be any real number or a constant from F. These constraints do not involve terms built up with functional symbols. The semantics of the usual operations over the reals is expressed in a relational framework. This model allows us to avoid the drawbacks of other models in which variables represent intervals and thus are likely to be bounded and thereafter modified by successive applications of narrowing. We end the section by proposing an algorithm, very close to Arc-consistency, which given a finite set of constraints, applies narrowing to compute a fixed point whose form is a stable set of constraints. We prove that the algorithm is sound and always terminates.
We give in the next section two important results concerning the behaviour of narrowing functions with respect to union and intersection. These results are the basis of our study on efficient and correct computation of complex and non interval-convex relations. This captures a number of useful relations over the reals (equality, inequalities, disequality, addition, multiplication, absolute value, min and max, etc.), and also deals with integer and Boolean constraints. The concrete output of this work is the design of a successor to BNR-Prolog, which allows the programmer to express constraints on different domains in a unified framework:
X,Y: real, X element of [-2.5, 2.5], I,J: integer, I element of [0, +infinity), X*X - 2*I >= 1 + sin(Y), I*I + J*J = 1
B1, B2, B3 : boolean, B1 <= B3, (logical implication) (2 - B1 - B2) * (1 - B3 + B1) = 0, (if then else) 1 <= B1 + B2 + B3 <= 2 (Cardinality operator)
X1, Y1, X2, Y2 : real, (X1 + Y1 <= X2) \/ (X2 + Y2 <= X1) = 1, ((X1 >= 2) /\ (X2 >= 1)) => ((X1 = 3) \/ (X2 = 3)) = 1The last part of the paper gives numerous examples and computational results from a first prototype, using classical benchmarks (linear constraints on integers, Boolean constraints). New benchmarks are proposed for non-linear constraints over the integers. Also, mixed Boolean-numerical constraints are illustrated by the magic series problem [3, 10] and the bridge problem [10] (scheduling with disjunctive constraints).
2. J. G. Cleary, "Logical Arithmetic", Future Computing Systems, Vol 2, No 2, pp.125-149, 1987.
3. A. Colmerauer, "An introduction to Prolog III", in Comms of the ACM , 33(7):69, July 1990.
4. M. Dincbas, H. Simonis and P. Van Hentenryck, "Extending equation solving and constraints handling in LP", in Proc. Colloquium CREAS MCC, Austin, Texas, May 1987.
5. J. Jaffar and J.L. Lassez, "Constraint LP", in Proc. POPL, ACM, 1987.
6. J.H.M. Lee and M.H. van Emden, "Adapting CLP(R) to Floating Point Arithmetic", in Proc. of the Fifth Generation Computer Systems Conf., Tokyo, Japan, 1992
7. R.E. Moore, "Interval Analysis". Prentice Hall, 1966.
8. W. Older and A. Vellino, "Extending Prolog with Constraint Arithmetic on Real Intervals", in Proc. of the Canadian Conf. on Electrical and Computer Engineering, 1990.
9. G. Sidebottom and W. Havens, "Hierarchical Arc Consistency Applied to Numeric Processing in Constraint LP", in Computational Intelligence 8(4), Blackwell Publishers, 1992.
10. P. Van Hentenryck, "Constraint Satisfaction in LP", MIT Press, Cambridge, 1989.
Frédéric Benhamou Groupe d'Intelligence Artificielle Faculté des Sciences de Luminy, case 901 163 Avenue de Luminy 13288 Marseille Cedex 9, France Email: benham@gia.univ-mrs.fr William J. Older Bell Northern Research Computing Research Lab. PO Box 3511, Station C Ottawa, Ontario K1Y 4H7, Canada
|
|
|
|
|
|
|
|