University of Toronto - Winter 2020
Department of Computer Science

CSC 2512: Advanced Propositional Reasoning
Winter 2020

Course Information

Welcome to the Winter 2020 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:Friday 3:00pm to 4:00pm
 Email: fbacchus @ cs.toronto.edu

Meeting Time and Place: Tuesdays 2:00pm to 4:00pm, AB 115 (Astronomy & Astrophysics Building 50 St. George 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.
Course Evaluation: The course evaluation will consist on the following components:

  1. Assignments (two small assignments involving developing some algorithm and doing some modifications to existing solvers). Worth 25%
  2. Class participation (giving 5min overviews of papers we are reading, and participating in class discussion). Worth 25%
  3. Project. Investigating some material from the course in greater detail, or investigating the use of this material in a topic related to your research or interests.Worth 50%

Assignments

  1. Assignment 2 is now available (March 9th) due April 3rd
  2. Assignment 1 is now available (Feb 11) due March 2nd. The referenced papers are:
      1. Efficient CNF Encoding of Boolean Cardinality Constraints by Olivier Bailleux and Yacine Boufkhad (CP2003).
      2. SAT Encodings of the At-Most-k Constraint by Bittner, Thum, and Schaefer.
      3. Minisat git

    Lectures

    1. Lecture 1. Propositional logic basics. DP and DPLL.
    2. Lecture 2. Proof Systems, proof complexity.
    3. Lecture 3 Part I. CDCL SAT solvers (Part I). small updates Jan 28th
    4. Lecture 3 Part II. CDCL SAT solvers (Part II).
    5. Readings for Feb 4th.
      1. 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).
      2. A Lightweight Component Caching Scheme for Satisfiability Solvers by Knot Pipatsrisawat and Adnan Darwiche (Sat 2007)
      3. 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).
      4. Predicting Learnt Clauses Quality in Modern SAT Solvers., by Gilles Audemard, Laurent Simon (IJCAI 2009)
      5. Coverage-Based Clause Reduction Heuristics for CDCL Solvers, by Hidetomo Nabeshima and Katsumi Inoue (SAT 2017)
    6. Readings for Feb 11th.
      1. DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs, Nathan Wetzler, Marijn J.H. Heule, and Warren A. Hunt, Jr. (Sat 2014).
      2. Effective Preprocessing in SAT through Variable and Clause Elimination by Niklas Een and Armin Biere (SAT 2005)
      3. Speeding Up Assumption-Based SAT, Randy Hickey and Fahiem Bacchus (Sat 2019).
      4. Using Minimal Correction Sets to more Efficiently Compute Minimal Unsatisfiable Sets, by Fahiem Bacchus and George Katsirelos, (CAV 2015)
    7. Lecture 4. SMT
    8. Readings for March 3rd
      1. DPLL(T): Fast Decision Procedures, by Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli (CAV 2004)
      2. Z3str3: A string solver with theory-aware heuristics by Murphy Berzish, Vijay Ganesh, and Yunhui Zheng (FMCAD 2017)
    9. Lecture 5 (minor update March 9th). MaxSat
    10. Readings for March 10th
      1. MiniMaxSat: A New Weighted Max-SAT Solver, by Federico Heras, Javier Larrosa, and Albert Oliveras, SAT 2007.
      2. RC2: an Efficient MaxSAT Solver, by Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva, Journal on Satisfiability, Boolean Modeling, and Computation 11 (2019) 53-64.
    11. Lecture 6 #Sat (counting models)
    12. Readings for March 24th
      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

    Other papers (may be moved to readings later)

    Last Term's Lectures

    1. Lecture 5. #SAT