CSC2512 Course Information University of Toronto - Winter 2018
Department of Computer Science

CSC 2512: Advanced Propositional Reasoning
Winter 2018

Course Information

Welcome to the Winter 2018 web page for CSC2512 a graduate course on Advanced Propositional Reasoning.

Instructor: Fahiem Bacchus
Office: D.L. Pratt 398E (6 King's College Rd)
Office Hours:Wed 4:00 to 5:00pm
Email: fbacchus @

Meeting Time and Place: Tuesdays 2:00pm to 4:00pm, AP 124 (Anthropology Building, 19 Russell Street).

Course Overview: We will examine current algorithms and techniques for solving various types of propositional reasoning problems. This will include the problems of finding a satisfying model (SAT), finding a satisfying model to a propositional formula augmented with a non-propositional formula over a decidable logical theory (SMT), finding an satisfying model that optimizes a specified cost function (MaxSat), counting the number of satisfying models (#SAT), and determining the truth or falsity of a closed quantified Boolean formula (QBF).

In each of these cases there have been considerable advances in developing solvers that are effective on many practical problems. (In general these problems are computationally intractable so no solver can be effective on all problems). Furthermore, since these problems are all complete for some well known complexity class it means that many other problems can be solved by efficient encodings.


  1. Lecture 1. Propositional logic basics. DP (ordered resolution).
  2. Lecture 2. Proof Systems, proof complexity DPLL.