À propos de ce cours

100 % en ligne

Commencez dès maintenant et apprenez aux horaires qui vous conviennent.

Dates limites flexibles

Réinitialisez les dates limites selon votre disponibilité.

Niveau intermédiaire

Approx. 10 heures pour terminer

Recommandé : 7 hours/week...

Anglais

Sous-titres : Anglais

100 % en ligne

Commencez dès maintenant et apprenez aux horaires qui vous conviennent.

Dates limites flexibles

Réinitialisez les dates limites selon votre disponibilité.

Niveau intermédiaire

Approx. 10 heures pour terminer

Recommandé : 7 hours/week...

Anglais

Sous-titres : Anglais

Programme du cours : ce que vous apprendrez dans ce cours

Semaine
1
1 heure pour terminer

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....
6 vidéos (Total 58 min), 2 lectures, 3 quiz
6 vidéos
Introduction to SAT7 min
SMT syntax and tools11 min
Eight queens problem9 min
Binary Arithmetic: addition10 min
Binary Arithmetic: multiplication12 min
2 lectures
Examples from the lecture10 min
Eight queens formula in SMT syntax10 min
3 exercices pour s'entraîner
Truth table2 min
Carries in binary addition2 min
Binary multiplication2 min
Semaine
2
17 heures pour terminer

SMT applications

This module shows a number of applications of satisfiability modulo the theory of linear inequalities (SMT)...
4 vidéos (Total 33 min), 2 lectures, 7 quiz
4 vidéos
Solving Sudoku7 min
Scheduling8 min
Bounded model checking8 min
2 lectures
Sudoku formula in SMT 2 format10 min
Introduction10 min
7 exercices pour s'entraîner
Rectangle fitting2 min
Scheduling2 min
Bounded Model Checking2 min
Filling trucks for a magic factorys
A sudoku variants
Job schedulings
Program correctnesss
Semaine
3
1 heure pour terminer

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....
6 vidéos (Total 56 min), 5 quiz
6 vidéos
Example of resolution8 min
DPLL10 min
Transforming DPLL to resolution9 min
CDCL basics11 min
CDCL optimizations6 min
5 exercices pour s'entraîner
Resolution2 min
apply resolution2 min
DPLL2 min
DPLL to resolution2 min
CDCL basics
Semaine
4
1 heure pour terminer

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....
6 vidéos (Total 55 min), 4 quiz
6 vidéos
The Tseitin transfomation10 min
Introduction to the Simplex method7 min
Optimizing by the Simplex method11 min
Checking feasibility by the Simplex method8 min
The Simplex method and SMT8 min
4 exercices pour s'entraîner
Transforming a propositional formula to CNF
The Tseitin transfomation
Slack form
Optimizing by the Simplex method

Enseignant

Avatar

Hans Zantema

prof.dr.
Department of Mathematics and Computer Science

À propos de EIT Digital

EIT Digital is a pan-European organization whose mission is to foster digital technology innovation and entrepreneurial talent for economic growth and quality of life. By linking education, research and business, EIT Digital empowers digital top talents for the future. EIT Digital provides online and blended Innovation and Entrepreneurship education to raise quality, increase diversity and availability of the top-level content provided by 20 leading technical universities around Europe. The universities deliver a unique blend of the best of technical excellence and entrepreneurial skills and mindset to digital engineers and entrepreneurs at all stages of their careers. The academic partners support Coursera’s bold vision to enable anyone, anywhere, to transform their lives by accessing the world’s best learning experience. This means that EIT Digital gradually shares parts of its entrepreneurial and academic education programmes to demonstrate its excellence and make it accessible to a much wider audience. EIT Digital’s online education portfolio can be used as part of blended education settings, in both Master and Doctorate programmes, and for professionals as a way to update their knowledge. EIT Digital offers an online programme in 'Internet of Things through Embedded Systems'. Achieving all certificates of the online courses and the specialization provides an opportunity to enroll in the on campus program and get a double degree. Please visit https://www.eitdigital.eu/eit-digital-academy/ ...

Foire Aux Questions

  • Une fois que vous êtes inscrit(e) pour un Certificat, vous pouvez accéder à toutes les vidéos de cours, et à tous les quiz et exercices de programmation (le cas échéant). Vous pouvez soumettre des devoirs à examiner par vos pairs et en examiner vous-même uniquement après le début de votre session. Si vous préférez explorer le cours sans l'acheter, vous ne serez peut-être pas en mesure d'accéder à certains devoirs.

  • Lorsque vous achetez un Certificat, vous bénéficiez d'un accès à tout le contenu du cours, y compris les devoirs notés. Lorsque vous avez terminé et réussi le cours, votre Certificat électronique est ajouté à votre page Accomplissements. À partir de cette page, vous pouvez imprimer votre Certificat ou l'ajouter à votre profil LinkedIn. Si vous souhaitez seulement lire et visualiser le contenu du cours, vous pouvez accéder gratuitement au cours en tant qu'auditeur libre.

D'autres questions ? Visitez le Centre d'Aide pour les Etudiants.