Satisfiability, Boolean Modeling and Computation

582742
5
Algoritmit ja koneoppiminen
Syventävät opinnot
Vuosi Lukukausi Päivämäärä Periodi Kieli Vastuuhenkilö
2015 kevät 11.05-22.05. 4-4 Englanti Matti Järvisalo

Luennot

Aika Huone Luennoija Päivämäärä
Ma 12-14 B222 Matti Järvisalo 11.05.2015-22.05.2015
Ke 12-14 B222 Matti Järvisalo 11.05.2015-22.05.2015
Pe 12-14 B222 Matti Järvisalo 11.05.2015-22.05.2015

Harjoitusryhmät

Group: 1
Aika Huone Ohjaaja Päivämäärä Huomioitavaa
Pe 14-15 B222 Jeremias Berg 11.05.2015—22.05.2015
Ke 14-15 B222 Jeremias Berg 11.05.2015—22.05.2015
Ma 14-15 B222 Jeremias Berg 11.05.2015—22.05.2015

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 intensive 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: 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: No formal prerequisites. Students are assumed to have good knowledge of basic concepts related to algorithms, computation, and artificial intelligence from the suitable bachelor's-level courses in computer science. The course is primarily intended for master's-level students and postgraduate students.

Kurssin suorittaminen

Active participation in lectures and tutorials, home assignments and a home exam.

Home exam (in pdf), deadline: June 8. For instructions, see the pdf.

Kirjallisuus ja materiaali

Lectures

Note: the lecture slides are preliminary versions, and will be updated after all lectures.

  1. Introduction and background, basic concepts [slides in pdf]
  2. Modern SAT solver algorithms: CDCL [slides in pdf]
  3. Preprocessing [slides in pdf]
  4. Boolean modeling [slides in pdf]
  5. Incremental SAT-based computation, Maximum satisfiability [slides in pdf]
  6. SAT-based counterexample-guided abstraction refinement [slides in pdf]
    SAT-based CEGAR for argumentation: Johannes Wallner gives a presentation on Complexity-Sensitive Decision Procedures for Abstract Argumentation. W. Dvořák, M. Järvisalo, J.P. Wallner, and S. Woltran. Artificial Intelligence 206:53-78, 2014.

 

Tutorials

  1. tutorial [sheet in pdf]
  2. tutorial [sheet in pdf]
  3. tutorial [sheet in pdf]
  4. tutorial [sheet in pdf]
  5. tutorial: Applications of MaxSAT. Jeremias gives a presentation on the paper Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability, J. Berg, M. Järvisalo, and B. Malone. Proc. 17th International Conference on Artificial Intelligence and Statistics (AISTATS 2014).
  6. tutorial: Overview of the home exam (by Matti)