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 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.