Applied Computational Engines

Summer Terms 2015, 2016, and 2017

Analyzing computational problems is at the heart of computer science. For example, the computational complexity of a problem tells us lower bounds on the running times and space requirements of the algorithms that we design to solve a problem. Likewise, the theoretical treatment of bijective functions tells us that we cannot design a data compression algorithm that is able to compress any possible data stream.

Yet, it can be observed that such theoretical limits are routinely ignored in practice. For example, modern data compression tools are able to shrink the size of a lot of files that can be found in the field. Such tools make use of the regular structure of many types of files, and are surprisingly robust in doing so. The existence of such tools does not contradict theory, however. In fact, when considering a random uniform distribution over the possible files of some length k, they are unable to compress most of the files. Yet, due to the high number of cases in which they do work, they are a valuable tool for the practitioner.

Data compression is an example which shows that despite the results from theory, there exist algorithms for some problems that can perform remarkably well on many problem instances found in the field. It may or may not come as a surprise that similar observations were made in other contexts as well. For example, many problems in operations research and formal verification are essentially search problems, and they are often NP-complete. Problems from this complexity class are often considered to be intractable in the literature. Yet, they are solved routinely in practice nowadays, which may seem to be a contradiction at first.

The key to this success is the application of modern computational engines. These are algorithms that efficiently solve comparably generic problems and allow many other problems to be encoded as input to the computational engine. They make use of the structure in their input instances, and typically yield exact results quickly on highly structured input instances.

An example computational engine is a satisfiability (SAT) solver, which is commonly applied when formally verifying two combinational circuits to be functionally equivalent. A SAT solver takes a boolean formula as input and checks whether there exists some valuation to its variables that makes the formula satisfied. The behavior of the two circuits can be represented as such a formula, and by a clever encoding, a valuation to the variables then represents an input signal valuation to the circuits on which their outputs differ. If the resulting boolean formula is then found to be unsatisfiable, this constitutes a proof of equivalence of the two combinational circuits from which we built the formula.

Apart from computational engines for problems that are NP-complete (or even harder), there also exist computational problems for some generic problems that are known to be solvable in polynomial time. Prime examples for this are linear programming and maximum flow algorithms. Many problems from operations research and other fields can be reduced to linear programming or maximum flow problems.

Computational engines do not replace theory. All impossibility and hardness results for some problem of course still apply. Also, computational engines do not replace the approximation algorithms that have been developed for some problems, and they also do not replace modern exact exponential-time algorithms that have been developed for commonly studied problems such as the traveling salesperson problem. Rather, they augment these results by providing platforms that are robustly usable for many practical problems. For an approximation algorithm, whenever we change a part of the problem, the algorithm is typically no longer applicable. Computational engines, on the other hand, can deal with many variations of a problem - we typically only need to change the encoding of the problem at hand into their input problem instances for the engine. Thus, they are particularly useful for tackling difficult computational problems for which due to their unique properties, no specialized algorithms exist.

In this course, we study a variety of computational engines to tackle computationally difficult problems. The engines chosen to be in scope for this course have proven themselves to be well-suited for exploiting the structure of many practical problems. This makes the concepts taught in this course well-applicable to wide classes of challenges dealt with in practice. Apart from computational engines for problems with a high computational complexity, we also consider commonly used such engines for simpler problems.

For every computational engine, we consider the question what structure in a problem the engines exploit and how they deal with the residual difficulty of the problems. We also shed light on the basic working principles of the engines and best practices for applying them. Of course, known weaknesses of the computational engines will also be discussed.

At the end of the course, the successful participant will have a broad knowledge of methods to tackle difficult algorithmic problems and will be able to identify suitable methods to deal with such challenges whenever they arise in practice.

Bachelor's Project "Tackling Algorithmic Problems with Solvers"


Many computational problems in practice deal with the derivation of artifacts that can be relatively easily checked for correctness. Examples are the construction of schedules that adhere to certain restrictions and the solution of Sudokus. Other computational problems are a bit more tricky to deal with, such as the computation of Sudokus from scratch, and the automatic construction of correct sorting networks. These problems have in common that their solutions are not easy to check. To probe if a Sudoku has exactly one solution, it has to be solved, which is not trivial. Likewise, checking a sorting network's correctness is equivalent to checking if all sequences of elements are sorted correctly by it.

The advent of general-purpose solvers allows to deal with the former type of problems in a simple way: rather than building specialized Sudoku solvers of time scheduling programs, we can encode the search for solutions in a satisfaction problem over a set of variables and let the existing solver figure out a solution.

For the latter type of problem, where checking a solution is more difficult, suitable solvers exist, but they do not scale as well as the solvers for the former type of problems.

For example, computing a sorting network for only 6 values is already a very difficult problem in practice. Recently, new approaches for dealing with these types of problems have been developed, but a good understanding of when they work well and when they do not is missing so far.

In this project, we worked on closing this gap. We applied modern computational solvers to a variety of practical problems, including the minimal sorting network problem and the derivation of 2D barcodes that are optically similar to a given reference image.