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

CSC 2512: Advanced Propositional Reasoning
Winter 2019

Course Information


Welcome to the Winter 2019 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:Thursdays 3:30 to 4:30pm
Email: fbacchus @ cs.toronto.edu

Meeting Time and Place: Tuesdays 2:00pm to 4:00pm, BA 2159 (Bahen Building).

Office Hours: Wednesday 1:00pm to 3:00pm, DL 398E (Pratt). Wed 23rd I have to leave at 2pm

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.


Lectures


  1. Lecture 1. Propositional logic basics. DP and DPLL.
  2. Lecture 2. Proof Systems, proof complexity.
  3. Lecture 3. CDCL SAT solvers. (updated Feb 11th (with new material))
    Readings to be discussed Feb 5th. Students will be randomly called on to give a short summary of each paper then we will discuss the paper's contents in more detail.
    1. An Empirical Study of Branching Heuristics through the Lens of Global Learning Rate by Jia Hui Liang, Hari Govind, Pascal Poupart, Krzysztof Czarnecki, and Vijay Ganesh (Sat 2017).
    2. Randomization in Backtrack Search: Exploiting Heavy-Tailed Profiles for Solving Hard Scheduling Problems by Carla P. Gomes, Bart Selman, Ken McAloon, Carol Tretkoff (AIPS 1998).
    3. A Lightweight Component Caching Scheme for Satisfiability Solvers by Knot Pipatsrisawat and Adnan Darwiche (Sat 2007)
    4. Trimming while Checking Clausal Proofs by Marijn J.H. Heule, Warren A. Hunt, Jr., and Nathan Wetzler (FMCAD 2013).
  4. Lecture 3. CDCL SAT solvers. (updated Feb 11th (with new material))
    Readings to be discussed Feb 12th. Students will be randomly called on to give a short summary of each paper then we will discuss the paper's contents in more detail.
    1. Predicting Learnt Clauses Quality in Modern SAT Solvers., by Gilles Audemard, Laurent Simon (IJCAI 2009)
    2. Coverage-Based Clause Reduction Heuristics for CDCL Solvers, by Hidetomo Nabeshima and Katsumi Inoue (SAT 2017)
    3. Effective Preprocessing in SAT through Variable and Clause Elimination by Niklas Een and Armin Biere (SAT 2005)
  5. Lecture 3. Extracting Minimal Unsatisfiable Sets (updated Feb 11th (with new material))
    Readings to be discussed Feb 26th (after reading week).
    1. Using Minimal Correction Sets to more Efficiently Compute Minimal Unsatisfiable Sets, by Fahiem Bacchus and George Katsirelos, (CAV 2015)
  6. Lecture 4. SMT
    Readings to be discussed March 12th.
    1. DPLL(T): Fast Decision Procedures, by Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli (CAV 2004)
  7. Lecture 5. #SAT Slides fixed March 19th
    Readings to be discussed March 19th.
    1. Preprocessing for Propositional Model Counting, by Jean-Marie Lagniez and Pierre Marquis, AAAI-2014.
    2. Constrained Sampling and Counting: Universal Hashing Meets SAT Solving, by Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, and Sharad Malik. AAAI Workshop on beyond NP.
    3. On computing Minimal Independent Support and its applications to sampling and counting, by Alexander Ivrii, Sharad Malik, Kuldeep S. Meel, and Moshe Y. Vardi, CP-2015

Assignments


  1. Assignment 1. Out Feb 8th due March 4th
    1. MiniSat Git Repository where you can download the MiniSat solver. The MiniSat page also has some useful material.
    2. The Sat Competition 2007 industrial instances are suitable for solving with MiniSat (you will have to uncompress them before using MiniSat). The main page for the Sat competitions contains links to benchmarks from many different competition years. But MiniSat probably will be quite slow on the instances used in more recent competitions.


    Last Term's Notes and Assignments