Monthly Subscription Starting at AED 99 + VAT

Automated Reasoning: satisfiability
  • Level Professional
  • المدة 25 ساعات hours
  • الطبع بواسطة EIT Digital
  • Offered by

عن

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. 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.

الوحدات

General introduction

    • 1 Videos
Show info about module content

1 Videos

  • General introduction, and an application to poster printing

Introduction to SAT

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Truth table

1 Videos

  • Introduction to SAT

SMT+syntax+tools

    • 1 Videos
    • 1 Readings
Show info about module content

1 Videos

  • SMT syntax and tools

1 Readings

  • Examples from the lecture

Eight Queens Problem

    • 1 Videos
    • 1 Readings
Show info about module content

1 Videos

  • Eight queens problem

1 Readings

  • Eight queens formula in SMT syntax

Binary Arithmetic: addition

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Carries in binary addition

1 Videos

  • Binary Arithmetic: addition

Binary Arithmetic: multiplication

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Binary multiplication

1 Videos

  • Binary Arithmetic: multiplication

Rectangle fitting

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Rectangle fitting

1 Videos

  • Rectangle fitting

Solving Sudoku

    • 1 Videos
    • 1 Readings
Show info about module content

1 Videos

  • Solving Sudoku

1 Readings

  • Sudoku formula in SMT 2 format

Scheduling

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Scheduling

1 Videos

  • Scheduling

Bounded model checking

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Bounded Model Checking

1 Videos

  • Bounded model checking

Practical assignment

    • 1 Readings
    • 4 Assignment
Show info about module content

4 Assignment

  • Filling trucks for a magic factory
  • A sudoku variant
  • Job scheduling
  • Program correctness

1 Readings

  • Introduction

Resolution

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Resolution

1 Videos

  • Resolution

Example of resolution

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • apply resolution

1 Videos

  • Example of resolution

DPLL

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • DPLL

1 Videos

  • DPLL

Transforming DPLL to resolution

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • DPLL to resolution

1 Videos

  • Transforming DPLL to resolution

CDCL basics

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • CDCL basics

1 Videos

  • CDCL basics

CDCL optimizations

    • 1 Videos
Show info about module content

1 Videos

  • CDCL optimizations

Transforming a propositional formula to CNF

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Transforming a propositional formula to CNF

1 Videos

  • Transforming a propositional formula to CNF

The Tseitin transfomation

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • The Tseitin transfomation

1 Videos

  • The Tseitin transfomation

Introduction to the Simplex method

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Slack form

1 Videos

  • Introduction to the Simplex method

Optimizing by the Simplex method

    • 1 Videos
    • 1 Assignment
Show info about module content

1 Assignment

  • Optimizing by the Simplex method

1 Videos

  • Optimizing by the Simplex method

Checking feasibility by the Simplex method

    • 1 Videos
Show info about module content

1 Videos

  • Checking feasibility by the Simplex method

The Simplex method and SMT

    • 1 Videos
Show info about module content

1 Videos

  • The Simplex method and SMT

Auto Summary

Dive into the world of Automated Reasoning with this professional course focusing on satisfiability (SAT/SMT) tools. Led by expert instructors, you'll explore applications such as poster fitting, scheduling, and puzzle-solving, alongside foundational theories like the CDCL framework and the simplex method. With a mix of lectures, quizzes, and hands-on assignments, this 1500-minute Coursera course offers a robust learning experience for Data Science & AI enthusiasts. Ideal for professionals seeking practical skills and theoretical knowledge, with starter subscription options available.

Hans Zantema
Instructor

Hans Zantema