Satisfiability, Boolean Modeling and Computation

582742
5
Algoritmit ja koneoppiminen
Syventävät opinnot

Koe

09.03.2016 09.00 B123
Vuosi Lukukausi Päivämäärä Periodi Kieli Vastuuhenkilö
2016 kevät 19.01-03.03. 3-3 Englanti Matti Järvisalo

Luennot

Aika Huone Luennoija Päivämäärä
Ti 12-14 B222 Matti Järvisalo 19.01.2016-03.03.2016
To 12-14 B222 Matti Järvisalo 19.01.2016-03.03.2016

Harjoitusryhmät

Group: 1
Aika Huone Ohjaaja Päivämäärä Huomioitavaa
Ti 10-12 B119 Jeremias Berg 25.01.2016—04.03.2016

Yleistä

Boolean satisfiability (SAT), despite being an archetypical NP-complete problem, has today become a central paradigm for exactly solving various important computationally hard problems. This success is based on recent breakthroughs in practical implementations of decision procedures for SAT, i.e., SAT solvers, that are today used as core procedures in various industrial and AI applications, ranging from automated hardware and software verification, planning, and scheduling, to data analysis and automated mathematical theorem proving.

This 5-credit course gives an up-to-date coverage of central computational aspects of SAT, focusing on techniques that are important for modern real-world applications of SAT. Topics include: basics of propositional logic and computation; modern SAT solver algorithms and search techniques; preprocessing; modelling real-world problems as SAT; building complex SAT-based procedures for Boolean optimization and other search problems beyond NP.

Prerequisites: Students are assumed to have good background on algorithms, computation, and artificial intelligence from the suitable bachelor's-level courses in computer science. Knowledge of propositional logic is an asset. The course is primarily intended for algorithmically/mathematically oriented master's-level students and postgraduate students. Students majoring in mathematics interested in real-world applications of formal logic are also encouraged to attend.

Kurssin suorittaminen

The course consists of weekly lectures (4 h per week) and and six weekly tutorial sessions. Active participation in the lectures and tutorials is encouraged, as the final exam is based solely on the lectures and tutorials. In order to pass the course, students will need to independently solve a set of tutorial exercises and pass a final exam.

Kirjallisuus ja materiaali

The course material consists of the lectures, lecture slides, and the tutorials. The course is not based on any single book, and it is not necessary to purchase a book in order to successfully complete the course. 

Lectures

  1.  January 19: Introduction, basic concepts, background on propositional logic. Standard CNF translation. [pdf]
  2.  January 21: Background on complexity. Complete algorithms for SAT: DPLL, SAT solvers and resolution proof systems. [pdf]
  3.  January 26: Complete algorithms for SAT: CDCL. [pdf]
  4.  January 28: Preprocessing. Inprocessing. [pdf]
  5.  February 2: Boolean modeling. [pdf]
  6.  February 4: Incremental SAT solving. Minimal unsatisfiability I. [pdf]
  7.  February 9: Minimal unsatisfiability II: MUS extraction. [pdf]
     Note: no lectures during February 11-18
  8.  February 23:  Boolean optimization: Maximum satisfiability I. [pdf]
  9.  February 25: Maximum satisfiability II: Algorithms. [pdf
  10.  March 1: Counterexample guided abstraction refinement. Quantified Boolean formulas. Course summary. [pdf
  11.  March 3: "All questions answered"

Tutorials and Home Assignments

The weekly home assignment problems are included in the tutorial sheets. The deadline for returning solutions to the weekly home assignments is by the beginning of the tutorial session each week. More information is provided in the problem sheet for Tutorial 1.

  1. ​ January 26 [pdf]
  2.  February 2 [pdf]
  3.  February 9 [pdf]
  4.  February 16 [pdf]
  5.  February 23 [pdf]
  6.  March 1 [pdf]

Further Reading and Material

The topics considered on the course are based on recent developments in the field. As such, there is currently no suitable textbook available that would cover the contents of the course. However, various tutorial presentations (some with video recordings) as well as some surveys on topics covered on this course are available online. Some of these are listed here. Feel free to suggest additional links!

Further Links