CMP SCI 691SS - Seminar: Satisfiability Solvers and Their Applications - Spring 2008

  • Instructor: 
        J. Eliot B. Moss, Professor
    Office: Computer Science Building 372
    Email: moss at cs.umass.edu
    Phone: (413) 545-4206; Fax: (413) 545-1249
    Hours: by appointment (please do!)
  • Class schedule:
    Seminar: Mon/Fri 3:35-4:50 CMPS 142
    NOTE: Some Monday sessions may be "bumped" by faculty candidate talks, etc.

  • Description:

    Satisfiability (SAT) solvers are now widely available and have growing applications to a wide-range of computer science problems. In this seminar we will explore the state of the art in solver technology and also of applications to fields of interest, particularly computer architecture and software verification. We may also look at related problems such as Max-SAT and quantified boolean formulae. Students will offer concise presentation and critique of papers drawn from the literature. Students will also undertake projects in either extending a solver or applying one to a problem of their choosing. Grades will be based on quality of participation and on the project work. There are no particular prerequisites for this seminar beyond a basic appreciation of proof techniques and a desire to learn about these approaches to automated verification and optimization.

  • Requirements:

  • Read all papers chosen in this survey
  • Present and critique a fair share of the papers
  • Propose and carry out a project, either extending a SAT solver or using one on a suitable problem

  • Class Documents:

  • Schedule (private to class)
  • Link to SAT conferences in UMass library digital collections
    (you must be on campus or have a UMass OIT account to use this)

  • Presentation Materials (private to class members)
  • Draft list of papers
  • Course slides and tutorials gathered from the Internet


  • BiBTeX entries for papers: