Search algorithm | EPFL Graph Search

In computer science, a search algorithm is an algorithm designed to solve a search problem. Search algorithms work to retrieve information stored within particular data structure, or calculated in the search space of a problem domain, with either discrete or continuous values. Although search engines use search algorithms, they belong to the study of information retrieval, not algorithmics. The appropriate search algorithm to use often depends on the data structure being searched, and may also include prior knowledge about the data. Search algorithms can be made faster or more efficient by specially constructed database structures, such as search trees, hash maps, and database indexes. Search algorithms can be classified based on their mechanism of searching into three types of algorithms: linear, binary, and hashing. Linear search algorithms check every record for the one associated with a target key in a linear fashion. Binary, or half-interval, searches repeatedly target the cen

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the software's correctness, and that automatically generate code from a formal contract provided by the programmer, along with a proof of the generated code's correctness. In addition, recent technological developments have provided tools that have enabled researchers to revisit the synthesis problem. The recent rise of SMT solvers has given synthesis tools a reliable and automated way to verify synthesized programs against contracts. The introduction of counter-example guided inductive synthesis has provided researchers with a flexible synthesis algorithm that they can adapt according to their specific domain. In this dissertation, we develop new algorithms to synthesize recursive functional programs with algebraic data types from formal specifications and/or input-output examples. We manage to scale beyond the reach of other similar tools to synthesize nontrivial functional programs, with a focus on data structure transformations. First, we address the problem of precisely specifying the desired space of candidate programs, described by context free grammars (CFGs). We implement and evaluate a method for reducing the program space by describing axioms of the target language and other domain-specific restrictions on the level of the CFG, without explicitly generating and rejecting undesirable programs. We provide a method that extracts a program model from a corpus of code and that builds a probabilistic CFG from it. We showcase the usefulness, both individually and in tandem, of these methods. Second, we develop an algorithm to efficiently traverse a possibly unbounded space of candidate programs generated from a probabilistic CFG. This algorithm is an implementation of the A* best-first search algorithm on the derivation graph generated from the CFG, with a number of domain-specific optimizations. We evaluate the efficiency of the algorithm as well as the effectiveness of the optimizations. Finally, we describe a program repair framework that locates and fixes bugs in erroneous functional programs. Our novel fault localization technique detects erroneous snippets with concrete execution and eliminates false positives by analyzing dependencies between execution traces. After the erroneous code snippet is discovered, a modified version of our synthesis algorithm generates fixes for it by introducing modifications to the original erroneous code.

EPFL2019

Problèmes de cheminements optimaux dans les réseaux avec contraintes associées aux arcs

In this thesis we consider two optimal routing problems in networks. Both are NP-hard and are often used to modelize real life problems of large size. We first present the capacitated arc routing problem (CARP). In this problem, we have to serve a set of customers represented by the arcs of a network with vehicles of restricted capacity. The aim is to design a set of vehicle routes of least total cost. We describe two heuristic methods for the CARP based on local search techniques. The first one is a Tabu Search heuristic using an original post-optimization procedure. Principles appearing in this procedure are used to define a class of neighborhoods we combine in a Variable Neighborhood Descent method. Our algorithms compare favorably with some of her methods. They were initially developed to deal with the undirected CARP. We describe how to transform them so that they can be applied to the directed CARP. We also propose an adaptation to the directed case of a lower bound originally developed for the undirected CARP. This lower bound is used to evaluate the quality of the solutions produced by our algorithms for the directed CARP. Our methods obtain solutions whose value is, on average, close to known lower bounds. We use the CARP to tackle a real life problem of boat routing and scheduling. This problem can be viewed as a directed CARP with time windows. We describe in detail its modeling process and we analyze our first results. We obtain solutions that require less boats than the present schedule. Nevertheless, these solutions are not completely feasible in practice. We suggest some ways to improve them. The second problem treated in this thesis is the shortest capacitated paths problem (SCPP). We present a Tabu Search heuristic and some post-optimization procedures for the SCPP. These procedures are called in our Tabu Search algorithm. Two versions of this algorithm are considered. In the first one, post-optimization procedures are intensively used. In the second one, they are less frequently applied. This second version is faster. Compared with a greedy approach, the two versions of our Tabu Search heuristic obtain solutions which are, on average, of better quality. The SCPP was proposed to us by EDF (Electricité de France) in order to minimize the total length of the paths followed by cables in a nuclear power-station. It can also be viewed as a subproblem of the bandwidth packing problem (BWP) appearing in telecommunications.

EPFL2000

Problèmes de cheminements optimaux dans les réseaux avec contraintes associées aux arcs

EPFL2000

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

EPFL2019