Satisfiability, Boolean Modeling and Computation

582742
5
Algorithms and machine learning
Advanced studies
Year Semester Date Period Language In charge
2015 spring 11.05-22.05. 4-4 English Matti Järvisalo

Lectures

Time Room Lecturer Date
Mon 12-14 B222 Matti Järvisalo 11.05.2015-22.05.2015
Wed 12-14 B222 Matti Järvisalo 11.05.2015-22.05.2015
Fri 12-14 B222 Matti Järvisalo 11.05.2015-22.05.2015

Exercise groups

Group: 1
Time Room Instructor Date Observe
Fri 14-15 B222 Jeremias Berg 11.05.2015—22.05.2015
Wed 14-15 B222 Jeremias Berg 11.05.2015—22.05.2015
Mon 14-15 B222 Jeremias Berg 11.05.2015—22.05.2015

General

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.

Completing the course

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

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

Literature and material

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)