22c:295 - Seminar on Artificial Intelligence
Propositional Satisfiability (and Beyond)
Spring 2003
Course Syllabus
Instructor
Prof. Cesare Tinelli
201F MLH
335-0735
tinelli@cs.uiowa.edu
Office hours:
Wed 2:00-3:30pm, Fri 1:30-3:00pm, or by appointment.
Lectures
TuTh 3:55-5:10pm, 217 McLean Hall.
Prerequisites
Consent of instructor.
A good background in discrete math is required.
Previous familiarity with first-order logic and inference systems also is helpful.
Web Page
Most of the information about the class,
including handouts and reading assignments,
will be available from the class web site:
http://combination.cs.uiowa.edu/295/
Course Description
This edition of the seminar concentrates on one of
the fundamental problems in both artificial intelligence and
computer science:
the propositional satisfiability (SAT) problem.
This is a problem that is easy to state
(given a propositional formula, determine whether it is satisfiable),
but is very difficult to solve in practice.
In the first half of the course,
we will go over a number of techniques and systems developed for solving
the SAT problem.
In the second half, we will see some extensions of SAT,
and methods for solving those as well.
These extensions are interesting because of their applications in
mathematical reasoning, planning and scheduling,
software/hardware verification, and compiler optimization, among others.
Course Objectives
The main objective of this course is to expose you
to the main principles and techniques of SAT solving.
At the same time the course is designed to contribute
to your professional growth as a researcher by
-
developing your ability to read research papers critically,
by recognizing main points and contributions,
and identifying strengths and weaknesses;
-
refining your communication skills; in particular,
your ability to present research work to an audience,
and to discuss technical material with your peers;
-
stimulating your potential for original research.
These goals will be achieved mainly by means of
weekly readings, in-class discussions and presentations,
and course projects.
Assignments and Exams
You will be given weekly reading assignments and
will be expected to be able to discuss the readings in class.
Normally, the assignments will also require you to write
brief summaries and evaluations of the reading material.
Each week one of you will give a presentation to the class
on one of the papers in the readings.
The presentation will be subject to a written review by the other students.
There will be no exams in this course.
Projects
A substantial part of the course will be occupied by
a team project.
Teams of 2,3 people will be formed by the instructor.
Each team can choose a project among a list provided by the instructor
or can propose a project of its own, subject to the instructor's approval.
The course project can be
either a programming project,
consisting in designing and implementing (parts of) a SAT solver,
or a survey project
about a specific subtopic in satisfiability.
Each project will be concluded by a peer-reviewed, in-class presentation,
and will require the submission of a written report.
Textbook and Readings
There is no textbook for this class.
The list of the reading material,
both background references and assigned readings,
will be published on the course webpage as the course progresses.
Most of the assigned readings and
some of the background references will be available on-line.
Grading
The weighting of items in grade determination will be roughly
the following:
participation to class discussion 20%,
individual presentations 25%,
term project 55%.
Special Needs
The instructor must hear from anyone who has a disability
that may require some modification of seating, testing, or other class requirements
so that appropriate arrangements can be made.
Please see the instructor after class or during office hours.
Topic Outline
The outline is tentative and will be adjusted as necessary during the course
of the semester.
- Intro to Logic
- Syntax and semantics of propositional logic
- Syntax and semantics of first-order logic
- Normal form transformations
- Propositional Satisfiability
- k-SAT and phase transition
- Basic SAT techniques
- Tableaux-based methods
- DPLL-based methods
- Binary decision diagrams
- OBDDs
- applications
- Transition systems
- Temporal properties
- Temporal logic CTL
- Satisfiability Modulo Theories
- general framework
- extending existing SAT techniques
- Optimizations
- applications: mathematical reasoning
- applications: planning
- applications: verification
- applications: temporal logics