Automated Reasoning: satisfiability (Coursera)

Offered by EIT Digital,
Automated Reasoning: satisfiability (Coursera)

In this course you will learn how to apply satisfiability (SAT/SMT) tools to solve a wide range of problems. Several basic examples are given to get the flavor of the applications: fitting rectangles to be applied for printing posters, scheduling problems, solving puzzles, and program correctness. Also underlying theory is presented: resolution as a basic approach for propositional satisfiability, the CDCL framework to scale up for big formulas, and the simplex method to deal with linear inequallities.

Class Deals by MOOC List - Click here and see Coursera's Active Discounts, Deals, and Promo Codes.

The light weight approach to following this course is just watching the lectures and do the corresponding quizzes. To get a flavor of the topic this may work out fine. However, the much more interesting approach is to use this as a basis to apply SAT/SMT yourself on several problems, for instance on the problems presented in the honor's assignment.

Syllabus

WEEK 1
SAT/SMT basics, SAT examples
This module introduces SAT (satisfiability) and SMT (SAT modulo theories) from scratch, and gives a number of examples of how to apply SAT.

WEEK 2
SMT applications
This module shows a number of applications of satisfiability modulo the theory of linear inequalities (SMT)

WEEK 3
Theory and algorithms for CNF-based SAT
This module describes how a rule called Resolution serves to determine whether a propositional formula in conjunctive normal form (CNF) is unsatisfiable. It is shown how an approach called DPLL does the same job, and how it is related to resolution. Finally, it is shown how current SAT solvers essentially implement and optimize DPLL.

WEEK 4
Theory and algorithms for SAT/SMT
This module consists of two parts.
The first part is about transforming arbitrary propositional formulas to CNF, leading to the Tseitin transformation doing this job such that the size of the transformed formula is linear in the size of the original formula. The second part is about extending SAT to SMT, in particular to dealing with linear inequalities. It is shown how the Simplex method for linear optimization serves for this job; the Simplex method itself is explained in detail.

Go to Class
MOOC List is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

Related Courses

Machine Learning (Coursera) Coursera
Stanford University

Machine Learning (Coursera)

Machine learning is the science of getting computers to act without being explicitly programmed. In the past decade, machine learning has given us self-driving cars, practical speech recognition, effective web search, and a vastly improved understanding of the human genome. Machine learning is so pervasive today that you probably use it dozens of times a day without knowing it. Many researchers also think it is the best way to make progress towards human-level AI. In this class, you will learn about the most effective machine learning techniques, and gain practice implementing them and getting them to work for yourself. More importantly, you'll learn about not only the theoretical underpinnings of learning, but also gain the practical know-how needed to quickly and powerfully apply these techniques to new problems.

Sep 7th 2026
5-12 Weeks
Digital Signal Processing 1: Basic Concepts and Algorithms (Coursera) Coursera
École Polytechnique Fédérale de Lausanne

Digital Signal Processing 1: Basic Concepts and Algorithms (Coursera)

Digital Signal Processing is the branch of engineering that, in the space of just a few decades, has enabled unprecedented levels of interpersonal communication and of on-demand entertainment. By reworking the principles of electronics, telecommunication and computer science into a unifying paradigm, DSP is a the heart of the digital revolution that brought us CDs, DVDs, MP3 players, mobile phones and countless other devices.

Sep 14th 2026
4 Weeks
Practical Steps for Building Fair AI Algorithms (Coursera) Coursera
Fred Hutchinson Cancer Center

Practical Steps for Building Fair AI Algorithms (Coursera)

Algorithms increasingly help make high-stakes decisions in healthcare, criminal justice, hiring, and other important areas. This makes it essential that these algorithms be fair, but recent years have shown the many ways algorithms can have biases by age, gender, nationality, race, and other attributes. This course will teach you ten practical principles for designing fair algorithms. It will emphasize real-world relevance via concrete takeaways from case studies of modern algorithms, including those in criminal justice, healthcare, and large language models like ChatGPT. You will come away with an understanding of the basic rules to follow when trying to design fair algorithms, and assess algorithms for fairness.

Sep 14th 2026
4 Weeks
Cluster Analysis in Data Mining (Coursera) Coursera
University of Illinois at Urbana-Champaign

Cluster Analysis in Data Mining (Coursera)

Discover the basic concepts of cluster analysis, and then study a set of typical clustering methodologies, algorithms, and applications. This includes partitioning methods such as k-means, hierarchical methods such as BIRCH, and density-based methods such as DBSCAN/OPTICS. Moreover, learn methods for clustering validation and evaluation of clustering quality. Finally, see examples of cluster analysis in applications.

Sep 7th 2026
4 Weeks
Algorithms, Part II (Coursera) Coursera
Princeton University

Algorithms, Part II (Coursera)

This course covers the essential information that every serious programmer needs to know about algorithms and data structures, with emphasis on applications and scientific performance analysis of Java implementations. Part I covers elementary data structures, sorting, and searching algorithms. Part II focuses on graph- and string-processing algorithms.

Sep 14th 2026
5-12 Weeks
Digital Signal Processing 4: Applications (Coursera) Coursera
École Polytechnique Fédérale de Lausanne

Digital Signal Processing 4: Applications (Coursera)

Digital Signal Processing is the branch of engineering that, in the space of just a few decades, has enabled unprecedented levels of interpersonal communication and of on-demand entertainment. By reworking the principles of electronics, telecommunication and computer science into a unifying paradigm, DSP is a the heart of the digital revolution that brought us CDs, DVDs, MP3 players, mobile phones and countless other devices.

Sep 14th 2026
3 Weeks
An Introduction to Logic for Computer Science (Coursera) Coursera
University of Leeds

An Introduction to Logic for Computer Science (Coursera)

Logic plays a fundamental role in computer science. This course is designed to equip you with a solid understanding of the fundamental principles of logic and their relevance in the field of computer science. In this course, you'll explore proposition logic and discover its practical applications in problem-solving, algorithm design, and the development of intelligent systems. By engaging in hands-on exercises, exploring real-world examples, and participating in discussions, you'll develop strong logical reasoning and critical thinking skills.

Sep 21st 2026
2 Weeks
Problem Solving Using Computational Thinking (Coursera) Coursera
University of Michigan

Problem Solving Using Computational Thinking (Coursera)

Have you ever heard that computers "think"? Believe it or not, computers really do not think. Instead, they do exactly what we tell them to do. Programming is, "telling the computer what to do and how to do it." Before you can think about programming a computer, you need to work out exactly what it is you want to tell the computer to do. Thinking through problems this way is Computational Thinking. Computational Thinking allows us to take complex problems, understand what the problem is, and develop solutions. We can present these solutions in a way that both computers and people can understand.

Sep 14th 2026
5-12 Weeks