Practical SAT Solving -- CS 395t -- Announcement

Homepage: http://www.cs.utexas.edu/users/marijn/class/2013-spring/cs395t/cs395t.html
Homepage: http://www.cs.utexas.edu/users/hunt/class/2013-spring/cs395t/cs395t.html


     Unique Number:  53724
 Class Room Number:  CLA 0.124 (Map)
	Class Time:  Monday, 4:00 to 7:00 pm


       Instructors:  Marijn Heule & Warren A. Hunt, Jr.
   Office Location:  GDC S7.714 & GDC S7.818
      Office Hours:  Thursday, 4:00 to 6:00 pm
            E-mail:  marijn@cs.utexas.edu, hunt@cs.utexas.edu

Satisfiability (SAT) solvers now support a wide range of applications in fields such as formal verification, planning, and bio-informatics. We will present the state-of-the-art in SAT-solving techniques, and we demonstrate how these techniques are being used to solve a wide variety of search and analysis problems. In this seminar, we will investigate search procedures used in successful conflict-driven clause learning SAT solvers. Additionally, we will describe recent algorithmic developments, in particular we will present techniques used in today's strongest solvers. Students will gain an understanding of how modern SAT solvers are internally implemented.

The seminar is organized to expose students to contemporary, SAT-related problems so they may make research contributions. We begin by providing the necessary background. Students (generally in pairs) will choose a topic from open questions in the field, and then work toward making a contribution. We will give more specialized lectures on chosen topics and assignments. Relevant research papers will be assigned based on such topics, which student will present to the instructors and other students. The remainder of the semester will focus on SAT-related research. Students will be guided to implement or modify a SAT solver and evaluate their results. Ideally, student efforts will mature into publications.

The introductory lectures concern information regarding the assignments. The second half of the semester will focus on student progress on their respective assignments. Class participation is expected, and student grades will, in part, reflect each student's contributions. Not showing up for class is a sure way to have the class-participation grade lowered. A final report will be required, that will document the student's knowledge and results. The weighting of the grades for the various aspects of the course are: in-class presentations - 30%, the class project - 50%, and class participation - 20%.

Return to CS395t course homepage.