Solvers Principles and Architectures (SPA)

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

Software testing and formal verification, Machine learning, Operations research and planning

Prerequisites

Logic, Linear and Abstract Algebra, Programming Languages Theory, Graph Algorithms

Contents

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

Khalil Ghorbal