University of Toronto - Winter 2020
Department of Computer Science
CSC 2512: Advanced Propositional Reasoning
Welcome to the Winter 2020 web page for CSC2512 a
graduate course on Advanced Propositional Reasoning.
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:
- Assignments (two small assignments involving developing some
algorithm and doing some modifications to existing solvers). Worth 25%
- Class participation (giving 5min overviews of papers we are
reading, and participating in class discussion). Worth 25%
- 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%
- Assignment 2 is now available (March 9th) due April 3rd
- Assignment 1 is now available
(Feb 11) due March 2nd. The referenced papers are:
CNF Encoding of Boolean Cardinality Constraints by Olivier
Bailleux and Yacine Boufkhad (CP2003).
- SAT Encodings of the At-Most-k
Constraint by Bittner, Thum, and Schaefer.
- Minisat git
- Lecture 1. Propositional logic basics. DP and DPLL.
- Lecture 2. Proof Systems, proof complexity.
- Lecture 3 Part I. CDCL SAT solvers (Part I). small updates Jan 28th
- Lecture 3 Part II. CDCL SAT solvers (Part II).
- Readings for Feb 4th.
- 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).
A Lightweight Component Caching Scheme for Satisfiability
Solvers by Knot Pipatsrisawat and Adnan Darwiche (Sat
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).
- Predicting Learnt
Clauses Quality in Modern SAT Solvers., by Gilles Audemard, Laurent
Simon (IJCAI 2009)
Coverage-Based Clause Reduction Heuristics for CDCL Solvers,
by Hidetomo Nabeshima and Katsumi Inoue (SAT 2017)
- Readings for Feb 11th.
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs,
Nathan Wetzler, Marijn J.H. Heule, and Warren A. Hunt, Jr.
Preprocessing in SAT through Variable and Clause
Elimination by Niklas Een and Armin Biere (SAT 2005)
Speeding Up Assumption-Based SAT, Randy Hickey and Fahiem Bacchus (Sat 2019).
Minimal Correction Sets to more Efficiently Compute Minimal
Unsatisfiable Sets, by Fahiem Bacchus and George Katsirelos,
- Lecture 4. SMT
- Readings for March 3rd
- DPLL(T): Fast Decision
Procedures, by Harald Ganzinger, George Hagen, Robert
Nieuwenhuis, Albert Oliveras, and Cesare Tinelli (CAV 2004)
- Z3str3: A string solver with
theory-aware heuristics by Murphy Berzish, Vijay Ganesh, and
Yunhui Zheng (FMCAD 2017)
- Lecture 5 (minor update March 9th). MaxSat
- Readings for March 10th
- MiniMaxSat: A New Weighted Max-SAT Solver, by
Federico Heras, Javier Larrosa, and Albert Oliveras, SAT 2007.
- RC2: an Efficient MaxSAT Solver, by
Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva,
Journal on Satisfiability, Boolean Modeling, and Computation 11 (2019) 53-64.
- Lecture 6 #Sat (counting models)
- Readings for March 24th
- Preprocessing for Propositional Model Counting, by
Jean-Marie Lagniez and Pierre Marquis, AAAI-2014.
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.
- 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
- Lecture 5. #SAT