The University of Iowa
22c:295 - Seminar on Artificial Intelligence
Decision Procedures
Spring 2005
Course Syllabus
Instructor
Cesare Tinelli201F MLH
335-0735
tinelli@cs.uiowa.edu
Office hours: Mon 3:00-4:30pm, Wed 2:00-3:30pm, or by appointment.
Lectures
TuTh 3:55-5:10pm, 114 Blank Honors Center.
Prerequisites
Consent of instructor. Basic knowledge of first-order logic (aka predicate calculus) is necessary. Having taken 22c145 and/or 22c245 is useful but not required.
Web Page
Most of the information about the class, including handouts and reading assignments, will be available from the class web site:Course Description
In this course we will study decision procedures for the satisfiability of formulas in logical theories. Decision procedures have applications in several areas of artificial intelligence and computer science, including planning, scheduling, compiler optimization, and software and hardware verification.
We will discuss a number of different first-order theories, and look at algorithms for deciding the satisfiability of certain classes of formulas in these theories. We will then look at methods for combining decision procedures in a modular way to produce decision procedures for larger theories. The basic theories presented will include the theory of equality with uninterpreted functions, arithmetic (both real and integer), bit-vectors, arrays, and finite sets.
Course Objectives
The main objective of this course is to get familiar with a number of algorithms and approaches for deciding the satisfiability of certain classes of formulas, analyzing the strengths and weaknesses of each approach, their differences and similarities, and the possibility of combining them.
At the same time, the course is designed to contribute to the students' professional growth as computer scientists by
- developing their ability to survey existing research and read research papers critically;
- developing their ability to devise and run experiments, and analyze their results;
- refining their communication skills; in particular, the ability to present research work to an audience, and to discuss technical material with peers.
Assignments and Exams
There will be no exams in this course. Most of the homework, common to students taking the class for 1 credit hour or 3 credit hours, will be readings from course notes or research papers. There might be a few small written assignments during the semester for the 3 hour students.
Projects
Students registered for 3 hours will be required to complete a term project. This is an implementation-oriented project done in teams of up to three people, formed by the instructor. A number of possible projects will be proposed by the instructor later in the semester. They will most likely require the implementation of a decision procedure for a certain theory, and the integration of this procedure into a more general satisfiability checker developed by the instructor's research group. In addition to the implementation work and the experimental evaluation of the implementation, each project will require an in-class presentation and a final project report. For this project, proficiency in the programming languages C/C++ or ML is desirable. More details on the projects will be posted on the course web site.
Textbook and Readings
There is no textbook for this course. All the reading material will be available from the course web site as needed.
Grading
The weighting of items in grade determination will be approximately the following: participation to class discussion 30%, written assignments and project 60%.
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.
General Policies
This course is given by the College of Liberal Arts and Sciences (CLAS). This means that class policies on matters such as requirements, grading, and sanctions for academic dishonesty are governed by the CLAS. Students wishing to add or drop this course after the official deadline must receive the approval of the CLAS Dean. Details of the University policy of cross enrollments may be found at: http://www.uiowa.edu/~provost/deos/crossenroll.doc