[an error occurred while processing this directive]

<h2>School Program (Overview)</h2>

<!-- <span style="text-decoration: line-through;"></span> -->

<p>
<a href="slides/General.pdf">Slides</a> from the welcome &amp; general info session
(June 3, 09:00-09:15).
</p>

<p>
<table border="1">
<tr>
<td>&nbsp;</td>
<td><b>Wednesday</b></td>
<td><b>Thursday</b></td>
<td><b>Friday</b></td>
</tr>

<tr>
<td>&nbsp;</td>
<td><b>July 3rd</b></td>
<td><b>July 4th</b></td>
<td><b>July 5th</b></td>
</tr>

<tr>
<td>Time/Theme</td>
<td><b>Boolean Satisfiability</b></td>
<td><b>Satisfiability Modulo Theories</b></td>
<td><b>Special Topics</b></td>
</tr>

<tr>
<td><b>08:00-09:15</b></td>
<td><a href="photos/Registration.jpg">Registration</a></td>
<td>Registration</td>
<td>Registration</td>
</tr>

<tr>
<td><b>09:00-09:15</b></td>
<td><a href="photos/Niemela.jpg"><b>I. Niemelä:</b></a> Welcome</td>
<td>&nbsp;</td>
<td>&nbsp;</td>
</tr>

<tr>
<td><table>
<tr><td><b>09:15-11:00</b></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Franco.jpg"><b>J. Franco:</b></a></td></tr>
<tr><td>Foundations and</td></tr>
<tr><td>Theoretical Aspects of</td></tr>
<tr><td>Propositional</td></tr>
<tr><td>Satisfiability</td></tr>
<tr><td><a href="slides/Franco.pdf"><b>[slides]</b></a></td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Oliveras.jpg"><b>A. Oliveras:</b></a></td></tr>
<tr><td>SMT Theory and DPLL(T)</td></tr>
<tr><td><a href="slides/Oliveras.pdf"><b>[slides]</b></a></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Heule.jpg"><b>M. Heule:</b></a></td></tr>
<tr><td>Preprocessing</td></tr>
<tr><td><a href="slides/Heule.pdf"><b>[slides]</b></a></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
</tr>

<tr>
<td><table>
<tr><td><b>11:00-12:00</b></td></tr>
</table></td>
<td><table>
<tr><td><b>Lunch Break</b></td></tr>
</table></td>
<td><table>
<tr><td><b>Lunch Break</b></td></tr>
</table></td>
<td><table>
<tr><td><b>Lunch Break</b></td></tr>
</table></td>
</tr>

<tr>
<td><table>
<tr><td><b>12:00-13:45</b></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Marques-Silva.jpg"><b>J. Marques-Silva:</b></a></td></tr>
<tr><td>CDCL SAT Solvers and</td></tr>
<tr><td>SAT-Based Problem</td></tr>
<tr><td>Solving</td></tr>
<tr><td><a href="slides/Marques-Silva.pdf"><b>[slides]</b></a></td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Cimatti.jpg"><b>A. Cimatti:</b></a></td></tr>
<tr><td>Applications of SMT Solvers</td></tr>
<tr><td>Slides
        <a href="slides/Cimatti1.pdf"><b>[set1]</b></a>
        <a href="slides/Cimatti2.pdf"><b>[set2]</b></a>
        <a href="slides/Cimatti3.pdf"><b>[set3]</b></a></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Szeider.jpg"><b>S. Szeider:</b></a></td></tr>
<tr><td>Parametrized Complexity</td></tr>
<tr><td><a href="slides/Szeider.pdf"><b>[slides]</b></a></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
</tr>

<tr>
<td><table>
<tr><td><b>14:15-16:00</b></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Janhunen.jpg"><b>T. Janhunen</b></a> and</td></tr>
<tr><td><b>J. Rintanen:</b></td></tr>
<tr><td>Tutorial 1 on SAT</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Heljanko.jpg"><b>K. Heljanko</b></a> and</td></tr>
<tr><td><b>T. Junttila:</b></td></tr>
<tr><td>Tutorial 2 on SMT</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Beyersdorff.jpg"><b>O. Beyersdorff:</b></a></td></tr>
<tr><td>Proof Complexity</td></tr>
<tr><td><a href="slides/Beyersdorff.pdf"><b>[slides]</b></a></td></tr>
</table></td>
</tr>

<tr>
<td><table>
<tr><td><b>16:15-18:00</b></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Giunchiglia.jpg"><b>E. Giunchiglia:</b></a></td></tr>
<tr><td>SAT-Based Planning</td></tr>
<tr><td><a href="slides/Giunchiglia.pdf"><b>[slides]</b></a></td></tr>
<tr><td>&nbsp;</td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Moura.jpg"><b>L. de Moura:</b></a></td></tr>
<tr><td>Internals of</td></tr>
<tr><td>Modern SMT Solvers</td></tr>
<tr><td><a href="slides/Moura.pdf"><b>[slides]</b></a></td></tr>
<tr><td>&nbsp;</td></tr>
</table></td>
<td><table>
<tr><td><a href="photos/Schaub.jpg"><b>T. Schaub:</b></a></td></tr>
<tr><td>Modelling and Solving</td></tr>
<tr><td>in Answer Set</td></tr>
<tr><td>Programming</td></tr>
<tr><td><a href="slides/Schaub.pdf"><b>[slides]</b></a></td></tr>
</table></td>
</tr>

<tr>
<td><table>
<tr><td><b>18:00-20:00</b></td></tr>
</table></td>
<td><table>
<tr><td><b>&nbsp;</b></td></tr>
</table></td>
<td><table>
<tr><td><b>School Dinner</b></td></tr>
</table></td>
<td><table>
<tr><td><b>&nbsp;</b></td></tr>
</table></td>
</tr>

</table>

Photos: &copy; 2013 T. Junttila
</p>

<p>
All lectures take place in the CS Building (building #30 at Otaniemi
<a href="http://www.aalto.fi/en/about/campuses/campus_maps/">campus</a>)
<b>hall T1</b>.
</p>

<p>
<b>Street address:</b> Konemiehentie 2, Espoo, Finland
</p>

<h2>Pre-Instructions for Tutorials</h2>

<p>
The two tutorial sessions take place in the Maari Building
(building #17 at Otaniemi
<a href="http://www.aalto.fi/en/about/campuses/campus_maps/">campus</a>)
computer classrooms <b>A</b> and <b>C</b>, and <b>B</b> (in reserve).
</p>

<p>
<b>Street address:</b> Sähkömiehentie 3, Espoo, Finland
</p>

<p>
As our SAT/SMT solver in tutorials,
we will use <a href="http://z3.codeplex.com/">Z3</a> developed at Microsoft
through its <a href="http://python.org">python</a> interface.
</p>

<h3>Installing and using Python</h3>

<p>
&nbsp;<br>
You should have the Python programming language version 2.7.X
(<b>not</b> 3.X.X) installed in your machine.  If not, please follow
these <a href="http://python.org">instructions</a> 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 <b>text editor</b>, 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.
</p>

<h3>Installing and using Z3</h3>

<p>
&nbsp;<br>
The easiest way to start using Z3 is to install the precompiled
nightly build version by following the instructions found
<a href="http://z3.codeplex.com/">here</a>
(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.
</p>

<p>
What remains is to ensure that the Python interpreter can find Z3
by setting path variables appropriately:
<ul>
<li> If you are invoking Python from command line and
     you have installed the precompiled Z3 under directory
     <code>/my/z3/path</code>, just make sure that
     the directory <code>/my/z3/path/bin</code>
     is included in the <code>PYTHONPATH</code> environment variable.
<li> For instance, in the bash syntax, it is sufficient to issue
     the following command:<br>
     <code>export PYTHONPATH=$PYTHONPATH:/my/z3/path/bin</code>
<li> If you are using some IDE instead, please consult its manual to find
     out how external libraries are included.
</ul>
</p>

<!-- --------------------------------------------------------------------- -->

[an error occurred while processing this directive]