Solvers Principles and Architectures (SPA)


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.


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


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


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.


Khalil Ghorbal