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

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.


Lectures


  1. Lecture 1. Propositional logic basics. DP (ordered resolution).
  2. Lecture 2. Proof Systems, proof complexity DPLL.
  3. Lecture 3. CDCL SAT solvers. Readings:
    1. Geoffrey Chu, Aaron Harwood, Peter J. Stuckey, Cache Conscious Data Structures for Boolean Satisfiability Solvers. JSAT 6(1-3): 99-120 (2009).
    2. Effective Preprocessing in SAT through Variable and Clause Elimination. Niklas Een and Armin Biere SAT 2005: p61—75
    3. Gilles Audemard, Laurent Simonm, Predicting Learnt Clauses Quality in Modern SAT Solvers. IJCAI 2009: 399-404.
  4. Lecture 4. MaxSat. Readings:
    1. MiniMaxSat: A New Weighted Max-SAT Solver. Federico Heras, Javier Larrosa, and Albert Oliveras.
    2. Postponing Optimization to Speed Up MAXSAT Solving. Jessica Davies and Fahiem Bacchus.
    3. Maximum Satisfiability Using Core-Guided MAXSAT Resolution. Nina Narodytska and Fahiem Bacchus.
  5. Lecture 5. Intro to SMT. See also this slide deck by Leonardo de Moura (the developer of Z3). He also has an extensive set of other slide decks from other talks he has given (including talks on his more recent work on the Lean Theorem Prover) at this site.
  6. Lecture 6. QBF. Readings:
    1. Solving QBF with Counterexample Guided Refinement by Mikolas Janota, William Klieber, Joao Marques-Silva and Edmund Clarke
    2. CAQE: A Certifying QBF Solver by Markus N. Rabe and Leander Tentrup.
    3. Incremental Determinization by Markus N. Rabe and Sanjit A. Seshia.
  7. Lecture 7. #SAT. Also slides by Kuldeep Meel on a recent approach to approximate model counting. (Original slides are here). Readings:
    1. Preprocessing for Propositional Model Counting by Jean-Marie Lagniez and Pierre Marquis, AAAI-2014
    2. On Computing Minimal Independent Support and Its Applications to Sampling and Counting by Alexander Ivrii, Sharad Malik, Kuldeep S. Meel, and Moshe Y. Vardi  Constraints 21(1), 2016.
    3. Counting-Based Reliability Estimation for Power-Transmission Grids. by Leonardo Duenas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. AAAI-2017.

Assignments


  1. Assignment 2. Out March 14 due April 4th.
  2. Assignment 1. Out Feb 8th due March 2nd.
    1. Dimacs file format
      c
      c comment lines 
      c
      c 
      p cnf 5 3
      1 -5 4 0
      -1 5 3 4 0
      -3 -4 0
      
      The file can start with comments, that is lines begining with the character c. Right after the comments, there is the line
      p cnf nbvar nbclauses
      indicating that the instance is in CNF format; nbvar is the exact number of variables appearing in the file; nbclauses is the exact number of clauses contained in the file. Then the clauses follow. Each clause is a sequence of distinct non-zero numbers between -nbvar and nbvar ending with 0 on the same line; it cannot contain the opposite literals i and -i simultaneously. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables.
    2. MiniSat home page.
    3. SAT Encodings of the At-Most-k Constraint by Alan Frisch and Paul Giannaros