[an error occurred while processing this directive]

School Program (Overview)

Slides from the welcome & general info session (June 3, 09:00-09:15).

  Wednesday Thursday Friday
  July 3rd July 4th July 5th
Time/Theme Boolean Satisfiability Satisfiability Modulo Theories Special Topics
08:00-09:15 Registration Registration Registration
09:00-09:15 I. Niemelä: Welcome    
J. Franco:
Foundations and
Theoretical Aspects of
A. Oliveras:
SMT Theory and DPLL(T)
M. Heule:
Lunch Break
Lunch Break
Lunch Break
J. Marques-Silva:
CDCL SAT Solvers and
SAT-Based Problem
A. Cimatti:
Applications of SMT Solvers
Slides [set1] [set2] [set3]
S. Szeider:
Parametrized Complexity
T. Janhunen and
J. Rintanen:
Tutorial 1 on SAT
K. Heljanko and
T. Junttila:
Tutorial 2 on SMT
O. Beyersdorff:
Proof Complexity
E. Giunchiglia:
SAT-Based Planning
L. de Moura:
Internals of
Modern SMT Solvers
T. Schaub:
Modelling and Solving
in Answer Set
School Dinner
Photos: © 2013 T. Junttila

All lectures take place in the CS Building (building #30 at Otaniemi campus) hall T1.

Street address: Konemiehentie 2, Espoo, Finland

Pre-Instructions for Tutorials

The two tutorial sessions take place in the Maari Building (building #17 at Otaniemi campus) computer classrooms A and C, and B (in reserve).

Street address: Sähkömiehentie 3, Espoo, Finland

As our SAT/SMT solver in tutorials, we will use Z3 developed at Microsoft through its python interface.

Installing and using Python

You should have the Python programming language version 2.7.X (not 3.X.X) installed in your machine. If not, please follow these instructions and be sure to download the correct version (currently 2.7.5, not any 3.X.X). For writing python code you can use any text editor, and then use shell commands to run the code. If you prefer to use your favorite IDE with python support instead, you are free to do so.

Installing and using Z3

The easiest way to start using Z3 is to install the precompiled nightly build version by following the instructions found here (see the section on supported platforms). If this does not work, e.g., due to versions of libraries, it is also quite straightforward to compile Z3 from the respective source package.

What remains is to ensure that the Python interpreter can find Z3 by setting path variables appropriately:

[an error occurred while processing this directive]