Solvers Principles and Architectures (SPA)

Official homepage (with schedule)

Description

We attempt to draw the common principles behind a wide range of “solvers” abstracting away momentarily the underlying involved theories. By solver we intend a computer program or algorithm that solves a specific class of problems such as Boolean satisfiability, linear optimization or ideal membership problems. Such solvers are ubiquitous nowadays and are used widely far beyond the community of computer scientists and software engineers. The non existence of decision procedures or the intrinsic high complexity of certain problems do not prevent developing such solvers. On the contrary, they often help better understanding the tackled problems. The main objective of this course is to help students apprehend and somehow deconstruct a given solver into its main components and layers (architecture) as well as its computational paradigms (recursive, sequential, parallel, randomized etc.). We will in addition highlight important implementation aspects such as data structures and heuristics. Indeed, many solvers owe much of their success to smart programming than theoretical breakthroughs. All along the course, recent notable applications of various typical solvers will be discussed as to highlight their broad impact.

Keywords

SAT/SMT Solvers, Convex Optimisation, Interior Point Methods, Numerical Methods, Symbolic Computation

Prerequisites

Licence in mathematics or theoretical computer science or equivalent degree. Basic notions in logic, calculus, linear and abstract algebra, combinatorics and graph algorithms will be required.

Overview of a variety of algorithm approaches to problem solving

Learning outcomes

The main objective of the course would be to reduce as much as possible the opacity of a large class of nowadays used solvers.

Teacher