Pelleau Abstract Domains in Constraint Programming

1. Auflage 2015
ISBN: 978-0-08-100464-7
Verlag: Elsevier Science & Techn.
Format: EPUB
Kopierschutz: Adobe DRM (»Systemvoraussetzungen)

E-Book, Englisch, 176 Seiten

Constraint Programming aims at solving hard combinatorial problems, with a computation time increasing in practice exponentially. The methods are today efficient enough to solve large industrial problems, in a generic framework. However, solvers are dedicated to a single variable type: integer or real. Solving mixed problems relies on ad hoc transformations. In another field, Abstract Interpretation offers tools to prove program properties, by studying an abstraction of their concrete semantics, that is, the set of possible values of the variables during an execution. Various representations for these abstractions have been proposed. They are called abstract domains. Abstract domains can mix any type of variables, and even represent relations between the variables. In this work, we define abstract domains for Constraint Programming, so as to build a generic solving method, dealing with both integer and real variables. We also study the octagons abstract domain, already defined in Abstract Interpretation. Guiding the search by the octagonal relations, we obtain good results on a continuous benchmark. We also define our solving method using Abstract Interpretation techniques, in order to include existing abstract domains. Our solver, AbSolute, is able to solve mixed problems and use relational domains. - Exploits the over-approximation methods to integrate AI tools in the methods of CP - Exploits the relationships captured to solve continuous problems more effectively - Learn from the developers of a solver capable of handling practically all abstract domains

Marie Pelleau is a Doctorate in Computer Science at the University of Nantes, France. Her research interests include Constraint Programming and local research Constraint Programming (CP) to model and solve combinatory problems.

Autoren/Hrsg.

Pelleau, Marie

Leseproben

Introduction
Recent advances in computer science are undeniable. Some are visible, and others are less known to the general public: today, we are able to quickly solve many problems that are known to be difficult (requiring a long computation time). For instance, it is possible to automatically place thousands of objects of various shapes in a minimum number of containers in tens of seconds, while respecting specific constraints: accessibility of goods, non-crush, etc. [BEL 07]. Constraint programming (CP) formalizes such problems using constraints that describe a result we want to achieve (accessibility of certain objects, for example). These constraints come with efficient algorithms to solve greatly combinatorial problems. In another research area, semantics, abstract interpretation (AI) attacks an insoluble problem in the general case: the correction of programs. With strong theoretical tools developed from its creation (fixed-point theorems), AI manages to prove the properties of programs. In this area, the effectiveness of methods makes it possible for impressive applications to be solved: tools in AI have, for instance, managed to prove that there was no overflow error in the flight controls of the Airbus A380 which contains almost 500,000 lines of code. The work presented in this book is at the interface between CP and AI, two research areas in computer science with a priori quite different problematics. In CP, the goal is usually to obtain a good computation time for problems that are, in general, nondeterministic polynomial time (NP), or to extend existing tools to handle more problems. In AI, the goal is to analyze very large programs by capturing a maximum of properties. Despite their differences, there is a common concern in these two disciplines: identifying an impossible or difficult (computationally) space to compute precisely (the solutions set in CP and the semantics of the program in AI). It concerns computing the relevant overapproximations of this space. CP proposes methods to carefully surround this space (consistency and propagation), always with Cartesian overapproximations (boxes in n or n). AI uses often less accurate overapproximations but not only Cartesian: they may have various different shapes (not only boxes but also octagons, ellipsoids, etc.). These non-Cartesian approximations facilitate more properties to be captured. In this book, we exploit the similarities of these overapproximation methods to integrate AI tools in the methods of CP. We redefine tools in CP from notions of AI (abstract domains). This is not only an intellectual exercise. Indeed, by generalizing the description of overapproximations, there is a significant gain in the expressiveness of CP. In particular, the problems are treated uniformly for real and integer variables, which is not currently the case. We also develop the octagon abstract domain, showing that it is possible to exploit the relationships captured by this particular domain to solve continuous problems more effectively. Finally, we perform the opposite task: we define CP as an abstract operation in AI, and develop a solver capable of handling practically all abstract domains. I.1 Context
As mentioned before, the CP and AI have a common concern: computing efficiently and as accurately as possible an approximation of a difficult or impossible space. However, the issues and problems of these two areas are different, and hence so are their fields of application. I.1.1 Constraint programming
CP, whose origins date back to 1974 [MON 74], is based on the formalization of problems such as a combination of first-order logic formulas, i.e. the constraints. A constraint defines a relationship between the variables of a problem: for example, two objects placed in the same container have an empty geometric intersection, that is to say, a heavy object should be placed under a fragile object. This is known as declarative programming. CP provides efficient generic solution methods for many combinatorial problems. Academic and industrial applications are varied: job-shop scheduling problems [GRI 11, HER 11a], design of substitution tables in cryptography [RAM 11], scheduling problems [STØ 11], prediction of the ribonucleic acid (RNA) secondary structure in biology [PER 09], optical network design [PEL 09] or automatic harmonization in music [PAC 01]. One of the limitations of the expressiveness of CP methods is that they are dedicated to the nature of the problem: solvers used for discrete variable problems are fundamentally different from techniques dedicated to continuous variable problems. In a way, the semantics of the problem is different depending on whether one deals with discrete or continuous problems. However, many industrial problems are mixed: they contain both integer and real variables. This is, for example, the case of the problem of fast power grid repair after a natural disaster [SIM 12] to restore the power as quickly as possible in the affected areas. In this problem, we try to establish a plan of action and determine the routes that should be used by repair crews. Some of the variables are discrete; for example, each device (generator, line) is associated with a Boolean variable, indicating whether it is operational or not. Others are real, as the electrical power on a line. Another example of application is the design of the topology of a multicast transmission network [CHI 08]: we want to design a network that is reliable. A network is said to be reliable when it is still effective even when one of its components is defective, so that all user communications can pass into the network with the least possible delay. Again, some of the variables are integers (the number of lines in the network) while others are continuous (the flow of information passing over the network average). The convergence of discrete and continuous constraints in CP is both an industrial need and a scientific challenge. I.1.2 Abstract interpretation
The basis of AI was established in 1976 by Cousot and Cousot [COU 76]. AI is the theory of semantic approximation [COU 77b] in which one of the applications is programs proof. The goal is to verify and prove that a program does not contain a bug, that is to say, runtime errors. Industrial stakes are high. Indeed, many bugs have made history, such as the Year 2000 bug, or Y2K, due to system design error. On January 1, 2000, some systems showed the date of January 1, 1900. This bug may be repeated on January 19, 2038, on some UNIX systems [ROB 99]. Another example of a bug is that of the infamous inaugural flight of the Ariane 5 rocket, which, due to an error in the navigation system, caused the destruction of the rocket only 40 s after takeoff. Every day, new softwares are being developed, corresponding to thousands or millions of lines of code. To test or verify these programs manually would require a considerable amount of time. The soundness of programs cannot be proven in a generic way; thus, AI implements methods to automatically analyze certain properties of a program. The analyzers are based on operations on the semantics of programs, that is, the set of values that can be taken by the variables of the program during its execution. By computing an overapproximation of these semantics, the analyzer can, for example, prove that the variables do not take values beyond the permitted ranges (overflow). Many analyzers are developed and used for various application areas, such as aerospace [LAC 98, SOU 07], radiation [POL 06] and particle physics [COV 11]. I.2 Problematic
In this book, we focus on CP solving methods, known as complete, that find the solution set or prove that it is empty, if necessary. These methods are based on an exhaustive search of the space of all possible values, also called search space. Using operations to restrict the space to visit (consistency and propagation), these methods can be accelerated. Existing methods are dedicated to a certain type of variables, discrete or continuous. Facing a mixed problem, containing both discrete and continuous variables, CP offers no real solution and the techniques available are often limited. Typically, variables are artificially transformed so that they are all discrete as in the solver Choco [CHO 10], or all continuous as in the solver RealPaver [GRA 06]. In AI, analyzed programs often, if not always, contain different types of variables. Theories of AI integrate many types of domains, and helped develop analyzers uniformly dealing with discrete and continuous variables. We propose to draw inspiration from the work of the AI community on the different types of domains to provide new solving methods in CP. These new methods should be able, in particular, to approximate with various shapes and solve mixed problems. I.3 Outline of the book
This book is organized as follows: Chapter 1 gives the mandatory notions of AI and CP to understand our work and an analysis of the similarities and differences between these two research areas. Based on the similarities identified between CP and AI, we define abstract domains for CP in Chapter 2, with a resolution based on these abstract domains. The use of an example of abstract domain existing in AI in CP, the octagons, is detailed in Chapter 3. Chapter 4 deals with the solving method implementation details presented in Chapter 2 for octagons. Finally, Chapter 5 redefines the concepts of CP using the techniques...