Research Areas

Algorithm Engineering for Dynamic Graph Optimization Problems in Concrete Applications
Prof. Matthias MüllerHannemann; MartinLutherUniversität HalleWittenberg;
Prof. Dr. Karsten Weihe; Technische Universität Darmstadt
Project website
In many applications of graph algorithms or graph optimization problems, the graphs or the instances undergo frequent small changes. A graph is called dynamic if it is changed by a sequence of change operations. The goal of dynamic graph algorithms is to recompute optimal solutions after updates faster than by resolving from scratch.
The focus of this project is on several concrete applications of dynamic graph optimization problems, in particular
 speedup techniques for timedependent multicriteria shortest path problems in a dynamic scenario,
 realtime timetable information of train connections in case of delays caused by construction work, technical defects or other reasons,
 passengeroriented delay management in public transport.
Using techniques of Algorithm Engineering we aim at closing the current gaps to practical solutions.

Algorithm Engineering for Efficient Genome Comparison
Prof. Dr. Knut Reinert; Freie Universität Berlin
In the last two decades, the field of genomics has seen large changes, fueled by technological advances in sequencing technology. Nowadays, important large mammalian genomes (e.g. human, rat, mouse) are completely available. Maybe even more impressive, the time/cost to read genomic data has sunk by at four/five orders of magnitude. In the next years, the rate of generated data will continue to increase as the cost will continue to decrease.
Clearly, this huge amount of data calls for the usage of computers and algorithms and both have successfully been applied to support biologists in their work. Without the contribution of computer science and bioinformatics, the biological and medical advances driven by genomics would have been impossible.
The pioneering work in Bioinformatics is done very closely to the sequencing labs and biologists. There, it is most important for a computational result to be available quickly. As long as the result is not obviously lacking, the methodology of designing, implementing and evaluating the programs, respectively algorithms is not questioned. Often, sequence analysis programs are written with ad hoc heuristic, tailored to the one use case at hand. Besides some simple metrics like "number of aligned bases/genes", experimental evaluation is often limited to anecdotal considerations. One reason for this is the lack of established metrics.
Benchmarks for Read Mapping
Read Mapping is one key component for modern genomics. In the last decade, tens of papers have appeared on this topic, due to the large advances that have been made in sequencing technology. Clearly, it is important for Biologists and Bioinformaticians to select a good read mapper objectively. However, most published read mappers solve slightly different problems.
Beginning from a precise definition of the problem of read mapping we are developing a precise formulation of a solution to this problem. Using these precise formulations, we are then designing algorithms and writing programs to evaluate read mapping programs in a fair and objective manner. These are then tied together by wrapping scripts to provide a comprehensive read mapping benchmark.
Whole Genome Comparison
Complex models that capture each and every biological detail quickly become computationally intractable. Simple models, however, are vulnerable to an excess of abstraction despite their ease of computability. These models can ultimately lead to efficient algorithms producing useless results. We plan to review approaches from the literature, create precise problem formulations from the whole genome alignment and comparison from these, introduce metrics for whole genome alignments and design/implement/evaluate (i.e. engineer) algorithms that solve these problems.

Algorithm Engineering for MONET and related covering problems
Prof. Dr. Martin Mundhenk; University of Jena
Project website
Given two monotone boolean formulae in different normalforms, i.e. conjunctive and disjunctive normalform, the problem Monet asks about the equivalence of these two formulae. Without the restriction that both monotone formulae are given in different normalforms, the problem becomes coNPcomplete in case of arbitrary monotone formulae or trivial in case of equal normalforms. Furthermore, the problem is coNPcomplete for arbitrary boolean formlae in normalform. There is nothing known about the exact complexity of Monet, neither a polynomial upper bound nor a nontrivial lower bound. There are many algorithms for the decision and the computation problem  the best upper bound is quasipolynomial in the length of input and output.
In particular, we want to compare the important algorithms, in due consideration of algorithm engineering. With this comparison, we hope for more information on hard instances for these algorithms and want to improve them. Also, there are many questions about new methods, e.g. randomization, multiplication and kernelization.
The area of applications in theory and practice is wide. Thus, we hope for many real world instances, e.g. from data mining or ecommerce.
In summary, our goals are Implementation and comparison of several known algorithms, in due consideration of algorithm engineering
 "Upgrades" for these algorithms, e.g. easy cases and data structures
 Creation of a testlibrary with miscellaneous instances
 New methods for solving the problem, e.g. randomization, multiplication and kernelization

Algorithm Engineering for Network Problems
Prof. Dr. Susanne Albers; AlbertLudwigsUniversität Freiburg
Project website

Algorithm Engineering for Problems in Computer Graphics
Prof. Dr. math. Friedhelm Meyer auf der Heide, Dr. rer. nat. Matthias Fischer; Universität Paderborn
Project website

Algorithm Engineering for Randomized Rounding Procedures
Prof. Dr. Benjamin Doerr; MaxPlanckInstitut für Informatik, Saarbrücken
Project website
Randomized rounding is one of the core methods of randomized computation, and is at the heart of many algorithms with good theoretical properties. However, despite this, and despite the long roots of the theoretical method, it seems that the performance of the method has scarcely ever been empirically evaluated, and implementations of the method are found only in isolated special cases.
Moreover, recent theoretical developments have extended the range of applicability of the method to include further ranges of problems, such as the problem of multicommodity flow, by providing methods of rounding which allow certain conditions (socalled hard constraints) to be maintained with a guarantee. Different approaches have been suggested for this, in some situations without any obvious a priori indications of one being preferable to the other, making the need for empirical evaluations and comparisons stronger.
One aim of the project is thus to provide these muchneeded empirical evaluations, comparing the methods both to one another and to other suggested methods (not of the randomized rounding type); another is to, based on the outcome of this, further the implementation and design of rounding algorithms to practical maturity.
One particular application where randomized rounding tools have seen some recent use is the creation of good sets of sampling points ( lowdiscrepancy point sets) in the highdimensional unit cube, which is needed in e.g. numerical integration problems. This topic is also part of our work.

Algorithm Engineering for Realtime Scheduling and Routing
Prof. Dr. Friedrich Eisenbrand; École Polytechnique Fédérale de Lausanne
Prof. Dr. Martin Skutella; Technische Unversität BerlinProject website
While 20 years ago, microprocessors have mostly been used in desktop computer workstations and largescale computers they have meanwhile become ubiquitous. They are used in nearly all areas of technology and specifically in safety and mission critical applications. The future vision of the automotive and avionics industry is complete, safe and reliable drivebywire and flybywire respectively. Such industrial applications gave rise to the field of computer science which is called realtime scheduling and routing. Whereas classical scheduling deals with the distribution of a finite set of tasks to a set of machines, realtime scheduling deals with recurring tasks which are often periodic and thus appear infinitely often. Since the processors in a realtime system communicate by passing messages, the messages have to be routed through the architecture (modeled as a directed graph) additionally.
The goal of the project is to develop, implement, analyze and test algorithms for realtime scheduling and routing problems using methods of linear and integer programming as well as various scheduling and routing techniques from discrete optimization.

Algorithm Engineering for the Basic Toolbox
Prof. Dr. Peter Sanders; Karlsruhe Institute of Technology
Project website
This project addresses algorithm engineering for basic algorithms and data structures that are the most important building blocks for many computer applications — sorting, searching, graph traversal,. . . . Although this topic is as old as computers science itself, many interesting new results have appeared in recent years and many gaps between theory and practice remain. In particular, many interesting approaches have not been thoroughly tried experimentally. Ever more complex hardware with memory hierarchies and several types of parallel processing requires reﬁned models, new algorithms, and efﬁcient implementations. We plan to incorporate the most successful implementations into reusable software libraries such as the the C++ STL.

Algorithms for Complex Scheduling Problems
Prof. Dr. Rolf H. Möhring; Technische Universität Berlin
Project website
Realworld scheduling problems are usually much more complex than most of the models that were considered in algorithm theory so far. Typically, optimal solutions cannot be found in reasonable computing time. However in practice, good solutions have to be computed fast. To meet the runtime requirements, mostly (simple) heuristics are established in industry, not taking into account results and techniques that are know for related theoretical problems. We aim to fill this gap between theory and practice, considering the following fields of scheduling:
 Combined Sequencing and Scheduling
 Turnaround Scheduling
This necessitates investigations on the structure and complexity of these problems. In a second step, the insights need to be transferred into efficient algorithms that produce provably good solutions also for large realworld problems within an appropriate computing time. Realistic data is available from cooperations with T.A. Cook Consultants, Berlin, PSI Business Technology and Salzgitter Flachstahl GmbH? , and Sachsenmilch AG, respectively (10.000  100.000 activities for turnaround scheduling, and two examples from sequencing and scheduling, one from coil coating with 2040 coils, and another one from dairy industry with 3040 jobs).

Algorithms for Modern Hardware: Flash Memory
Prof. Dr. Ulrich Meyer; Universität Frankfurt
Project website
Modern computers significantly deviate from the uniform cost model traditionally used in algorithms research. In the first phase of the proposed project we want to deal with a very recent trend: flash memory. Originally used in small portable devices, this block based solidstate storage technology is predicted to become a new standard level in the PC memory hierarchy, partially even replacing hard disks. Unfortunately, the read/write/erase performance of flash memory is highly dependent on access patterns, filling degree, and optimizations to prevent the devices from early wearout. Therefore, even cacheefficient implementations of most classic algorithms may not exploit the benefits of flash.
After appropriately modelling flash memory we aim at the design, analysis, implementation, and experimental evaluation of graph algorithms tailored to these models. We will cover both fundamental questions (like sorting, spanning trees, graph traversal, lower bounds) and applied problems (e.g. finding cycles in networks arising from cryptography applications) on massive graphs using flash memory. Some of these problems are still open for the easier externalmemory model, too, in particular for directed graphs, in dynamic or approximate setting. The best solutions will be added to libraries like STXXL. The potential benefits of this project are significantly improved methods to process largescale directed graphs like the web or social network graphs. Basic graph algorithms for depth first search, breadth first search, shortest paths, spanning trees or network flows are well established compenents of every algorithms course and many applications. Theory has produced advanced algorithms for these problems that should theoretically be superior to the simple text book methods. The starting point of this project is to explore the possibility to transform such advanced approaches in to practicable algorithms and implementations. We are particularly interested in algorithms that can exploit parallelism and memory hierarchies.

Clustering of Static and Temporal Graphs
Prof. Dr. Dorothea Wagner; Karlsruhe Institute of Technology
Project website
As a result of the rapidly growing extent of electronically available data, methods for the localization of relevant information and their intelligent organization are of increasing importance. The field of algorithmics is faced with the challenge of providing efficient and feasible algorithms for data clustering. This does not only encompass the development of algorithms that work well for specific applications or sets of data, but also the systematic design of algorithms for formally and rigorously defined problems and their analysis and evaluation with respect to adequate criteria of quality. In this project algorithms for the clustering of graphs shall be developed.
The focal point of our interest are clusterings which are based on the intuition of identifying as clusters dense subgraphs that are loosely connected among one another. To this end we shall underlay a systematic classification of quality measures, which allows for an unbiased comparison of various methodologies. In particular we will engage in the as yet novel field of clustering evolving or timedependent graphs. As far as possible, the evaluation of algorithms will be based on theoretical analyses, however, fundamentally it shall be conducted experimentally, namely employing suitably generated graphs on the one hand and taking into account real instances on the other hand. As usual in algorithm engineering, we shall traverse the entire cycle of design, analysis, implementation and experimental assessment, in particular reincorporating the results of experiments in the design and the analysis. Our implementations shall be made available in form of softwaretools consisting of algorithms, quality indices, measures and procedures of comparison, graph generators as well as benchmarks.
Software Projects
Further software projects can be also found here.

Design and Analysis of ApplicationOriented Geometric Algorithms
Prof. Dr. Helmut Alt; Freie Universität Berlin
Prof. Dr. Christian Knauer; Universität Bayreuth
Project website
The goal of this project is to close a gap between theoretically designed and studied algorithms and the methods that are widely used in practice, especially heuristics. We consider primarily but not exclusively the problem of the geometric shape matching. There are many algorithms and heuristic methods that work well and are widely used in practice but lack theoretical analysis. We analyze some of such heuristics with respect to the following questions:
 What is computed by the method? The quality of the computed results is often not known or even not clearly defined.
 What is the running time of the method? In many cases there is a certain tradeoff between the running time and the quality of results.
It might be necessary to constraint the inputs of the methods and to characterize the cases that occur in practice in order to be able to perform the analysis. Besides these theoretical studies we also plan to do prototype implementations of the designed algorithms to verify their practicability. The research focuses on the following problems:
 Patterns and shapes
 Probabilistic shape matching
 Symmetry detection
 Application oriented methods
 Packing and stacking geometric objects
 Realistic input models
 Geometric shape matching
 Geometric search structures
 Principal component analysis

Disturbed Diffusion for Partitioning and Clustering Graphs
Prof. Dr. Burkhard Monien; Universität Paderborn
Project website
Many natural and scientific transport phenomena can be modelled by diffusive processes. These processes perform exchanges of loads between neighboring entities in order to obtain a balanced load distribution. We have modified the first order diffusion scheme (FOS) on graphs with a suitable disturbance such that its convergence state results in a nonbalanced load distribution. These loads then reflect structural properties of the graph, which makes it possible to identify densely connected regions. This idea has been used successfully to develop an algorithm for graph partitioning and for balancing workloads of processors in parallel numerical simulations. Compared to classical methods, our new algorithm shows significant advantages regarding partitioning quality and migration costs. However, its running time is not satisfactory yet.
In this project we examine the new diffusionbased algorithm thoroughly on a theoretical and practical basis. We see promising approaches to solve the running time problems while keeping the quality improvements. This aims at the development of a graph partitioner which results in a signficantly more efficient parallel implementation and execution of parallel adaptive numerical simulations than before. Apart from that, the disturbed diffusion concept is also to be used for the automatic identification of tightly coupled groups (clusters) of different sizes in static and dynamic graphs and networks with local knowledge only. The resulting algorithms will be theoretically analyzed, implemented, parallelized, and finally, after a thorough experimental evaluation, made available as libraries. 
Efficient Search in Very Large Collections of Text, Databases and Ontologies
Prof. Dr. Hannah Bast; Universität Freiburg
Project website

Engineering of Approximation Algorithms for Matching and Covering in Hypergraphs and Large Graphs
Prof. Dr. rer. nat. Anand Srivastav; ChristianAlbrechtsUniversität Kiel
Project website
Matching in Hypergraphs
In the bmatching problem, we aim to select as many edges from a hypergraph as possible while allowing only b of them to overlap in each vertex. This problem and related ones have many applications in medicine, computational geometry, and combinatorial auctions. The bmatching problem is NPhard even if restricting to simplestructured instances. For large b, constantfactor approximations are achieved by randomized rounding. However, applications often demand small b. For small b, oblivious greedy algorithms are stateoftheart on the theoretical side; those incorporate graph parameters such as the number of vertices in the approximation guarantee.
A goal of our project is the development of nonoblivious algorithms that work well for small b, and better than the oblivious ones. We consider combinatorial and LPbased techniques, separately as well as in combination. At the same time, we improve the known inapproximability theory.
Matching in Large Graphs
With graphs containing a large number of edges, the random access model has to be reconsidered, since random access can result in excessive seek times. The new approach is to treat a graph as a stream of edges. Algorithms now cannot simply determine, e.g., whether two vertices are adjacent or not. Instead, algorithms have to make use of edges as they go by in the stream. They may pass over the stream multiple times, but the number of passes should be strictly limited.
In our project we design streaming algorithms for matching in bipartite and general graphs. In the first phase, we presented an approximation scheme for the bipartite case and proved a worstcase bound on the number of passes depending only polynomially on the approximation parameter. Ongoing research is concerned with experimentally analyzing and improving this algorithm. Moreover, the extension to general graphs is investigated.

Exact Integer Programming
Prof. Dr. Dr. h. c. Martin Grötschel; Zuse Institut Berlin
Project website
Available solvers for mixedinteger programs (MIPs) focus on finding close to optimal solutions for feasible instances. Users are aware that the answers are only accurate with respect to feasibility and optimality tolerances, but for many application, this is regarded to be acceptable.
This situation changes fundamentally when MIPs are used to study theoretical problems, when instances become pure feasibility questions (and are infeasible), and when wrong answers can have legal consequences. Examples for applications where inexact solvers are not adequate include combinatorial design theory, chip verification, and contracting by combinatorial auctions.
In this project, we develop and implement an approach for the exact solution of MIPs. By extending the constraint programming/MIP solver SCIP, we want to provide a tool, which is freely available to the scientific community, to compute exact optimal solutions or, perhaps even more important, exact certificates for infeasibility.

Generic Decomposition Algorithms for Integer Programs
Prof. Dr. Marco Lübbecke; RWTH Aachen University
Project website
There is no alternative to integer programming when it comes to computing proven quality or even optimal solutions to largescale hard combinatorial optimization problems. In practical applications, matrices often have special structures exploitable in decomposition algorithms, in particular in branceandprice. This opened the way to the solution of mixed integer programs (MIPs) of enormous size and complexity, both from industry and within mathematics, computer science, and operations research.
Yet, as the stateoftheart, branchandprice is implemented ad hoc for every new problem. Various frameworks are very helpful in this respect, still, this requires a solid expert knowledge. This project aims at making a significant contribution towards a generic implementation of decomposition algorithms. As a longterm vision, a MIP solver should be able to apply a decomposition algorithm without any user interaction. A precondition for such an automation is the answer to important algorithmic and theoretical questions, among them:
 recognition of decomposable structures in matrices and/or MIPs
 development of a theory (and appropriate algorithms) for evaluating the quality of a decomposition
In this project we address these questions. From a mathematical point of view, there are interesting relations to polyhedral combinatorics, graph theory, and linear algebra. A generic implementation of our findings is planned to be provided to the research community. To this end we closely cooperate with developers of MIP solvers (such as SCIP) and modeling languages (such as GAMS).

Kunst!  Exact Algorithms for Art Gallery Variants
Dr. Alexander Kröller; Braunschweig Institute of Technology
Project website
The classical Art Gallery Problem asks for the minimum number of guards that achieve visibility coverage of a given polygon. This problem is known to be NPhard, even for very restricted and discrete special cases. For the general problem (in which both the set of possible guard positions and the point set to be guarded are uncountable), neither constantfactor approximation algorithms nor exact solution methods are known. We develop a primaldual approach for general art gallery problems in arbitrary polygons with holes, in which guards can be placed anywhere, such that the entire interior of the polygon is guarded. Our method computes a sequence of lower and upper bounds on the optimal number of guards untilin case of convergence and integralityeventually an optimal solution is reached. Our algorithm is based on a formulation of the problem as a (covering) linear program. It solves the problem using a cutting plane and column generation approach, i.e., by solving the primal and dual separation problems. Computational results show the usefulness of our method.

Planarization Approaches in Automatic Graph Drawing
Prof. Dr. Michael Jünger; Universität zu Köln
Prof. Dr. Petra Mutzel; Universität DortmundProject website
This automatic graph drawing project concerns the transfer of planarization approaches that have been used primarily in academia so far, to practical applications. We consider a selection of important usecases, and we try to address the problems arising in these applications. We integrate various application specific constraints into the planarization method, and we provide open source software (see OGDF library) as well as benchmarks instances.
Currently, the application domains include visualization in software engineering and biochemistry, e.g. the visualization of metabolic and protein interaction networks. We will continuously apply the algorithm engineering cycle to our results, so that the engineering process is significantly influenced by the feedback from our cooperation partners. 
Practical Approximate Pattern Matching with Index Structures
Prof. Dr. Ernst W. Mayr, Technische Universität München
Project website
In this research project we apply the whole spectrum of algorithm engineering to index structures for approximate pattern matching. In contrast to the case of exact searching there is a big gap between theory and practice for the approximate case. We want to close this gap with our project. Some of the approaches which yield theoretical advances, seem to be not applicable in practice due to big constants.
A library of pattern matching algorithms would be of great benefit for other researches and computer scientists, providing efficient methods for indexbased approximate pattern matching. The library is supposed to be an interface for the ongoing progress in the field of indexes and algorithms. The implementations form a working basis for the further algorithm engineering process, but as well can be used by e.g. biologists to solve real world problems, like analyzing biological data. The library is supposed to offer index structures and search algorithms, developed and optimized espacially considering the following aspects:
 Efficient applicability to for big, real world problem instances, while using general and flexible error models.
 Index structures and search algorithms in secondary memory.
 Distributed index structures and search algorithms.
 Cacheefficient search algorithms.

Practical theory for clustering algorithms
Prof. Dr. rer. nat. Johannes Blömer, Universität Paderborn
Prof. Dr. rer. nat. Christian Sohler, TU Dortmund
Project website
Clustering is the partition of a set of objects into subsets (cluster) such that objects inside one cluster are similar to each other while objects from different clusters are not. In order to compute such a partition it is required to define what is meant by similarity. E.g. if we have a map and choose the recorded cities as our set of objects, we can interpret a short distance between the cities as similarity. Then the clustering corresponds to a division of our map into urban areas. Clustering algorithms try to compute clusterings that are as good as possible. One application area is data reduction. For that purpose every cluster is replaced by a proper substitute.
In a research project aided by the DFG we concentrate on two aspects. On the one hand we analyse algorithms of widespread use in order to find out how good or bad they are in theory. On the other hand we try to design provably good algorithms. Particular similarity measures like asymmetric measures are of special interest throughout our examination. One example of an asymmetric measure is the KullbackLeibler divergence that enables us to talk about the similarity of probability distributions. The figure shows the asymmetry of the KLD. The two colored curves have the same distance to the marked center, in one case measured from the curve to the center and in the other case the other way around.

Representation Solving
Prof. Dr. Alexander May; RuhrUniversität Bochum
Project website
For many NP hard problems like the subset sum problem, syndrome decoding or the computation of a shortest vector in a lattice we basically know algorithms which perform not much better than a simple brute force search over the solution space. This might serve our intuition that we actually expect exponential complexity for NP hard problems in general.
There are few general techniques that help to lower the running time exponent. One of them is the socalled sort and match technique, where the search space is splitted in two parts of equal size. This technique can be used to obtain a time memory tradeoff, e.g. instead of complexity O(2^n) and constant space we obtain O(2^{\frac n 2}) both for time and space.
In 2010, HowgraveGraham and Joux presented another technique, that we call the representation technique, in the context of solving the subset sum problem. The idea is to represent the solution of a subset sum in an ambiguous way which results in an exponential number of representations. Out of this exponential number, one looks for a special unique solution, again. Surprisingly, this blowupandcut strategy helped HowgraveGraham and Joux to lower the subset sum complexity from O(2^{0.5n}) to O(2^{0.337n}).
Our goal is give a general analysis of the representation technique that allows to apply the technique as a generic algorithmic tool in various contexts. Our first application is an improvement of the best known algorithm for decoding general linear codes, for which we can significantly lower the complexity. Further applications of the representation technique are among others the computation of shortest vectors and a new combinatorial algorithm for a hard problem in cyclic lattices that is underlying the NTRU encryption scheme. 
RoboRithmics: Algorithmical and Technical Methods for Controlling an Autonomous Exploration Robot
Prof. Dr. Sándor Fekete; TU Braunschweig
Project website

Robust Optimization Algorithms
Prof. Dr. Anita Schöbel; GeorgAugustUniversität Göttingen
Project website
An exact optimal solution for an optimization problem is often useless for practical applications if the assumptions change or if unforeseen events occur. This is a reason for the gap between theory and practice in optimization. In the project Robust Optimization Algorithms we aim at improving this situation by developing robust algorithms which are applicable in practice. To this end it is necessary to adapt the robustness concepts and the algorithms to the problem instance and to the uncertainty type found in the data.

Simple and Fast Implementation of Exact Optimization Algorithms with SCIL
Prof. Dr. Ernst Althaus; Universität Mainz
Prof. Dr. Christoph Buchheim; Technische Universität DortmundProject website
SCIL is a software that allows a simple implementation of exact algorithms for difficult optimization problems. It is based on efficient BranchandCut procedures, but compared to other approaches it also supports symbolic constraints instead of linear inequalities.
The project's goal is further development of SCIL. We focus on the integration of new separation methods that will lead to a considerable speedup and to the development of new modelling possibilities. An important point is the ability to use polynomial objective functions and logic constraints. Moreover SCIL should be extended such that numerically exact optimal solutions could be computed  an important feature, e.g., for automatic verification of hybrid systems.
In order to ensure a practiceoriented development, another part of the project focuses on solving difficult practical optimization problems that are particularly well suited as applications for SCIL.

Structure Based Algorithm Engineering for SAT Solving
Prof. Dr. Michael Kaufmann, Prof. Dr. sc. techn. Wolfgang Küchlin; Universität Tübingen
Project website
Given a boolean formula the satisfiability problem (SAT) asks if there exists a truth assignment to the variables of the formula such that the formula evaluates to true. Even though this problem seems to be purely theoretical there are several realworld problems that can be formulated as a SAT problem like hardware and software verification, planning, automotive product configuration and problems in bioinformatics.
From the theoretical point of view SAT is NPcomplete and should thus be not solvable in feasible time. However, in the last 15 years stateoftheart SAT Solvers became able to tackle many realworld SAT instances with hundreds and thousands of variables.
We aim to improve SAT solving by analysing and enhancing current solving techniques. Our main goal is to allow for more structural analysis of instances during the solving process. Moreover, we implement and evaluate hybrid and parallel solving techniques to combine different successful approaches to one robust solver.
This work requires extensive evaluation and verification of the solver on huge sets of benchmarks. In the international SATcompetition 2009 our solver was able to win the silver medal in the category of satisfiable crafted instances.