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
- Lecture 1. Propositional logic basics. DP (ordered resolution).
- Lecture 2. Proof Systems, proof complexity DPLL.
- Lecture 3. CDCL SAT solvers. Readings:
- Geoffrey Chu, Aaron Harwood, Peter J. Stuckey, Cache
Conscious Data Structures for Boolean Satisfiability
Solvers. JSAT 6(1-3): 99-120 (2009).
- Effective
Preprocessing in SAT through Variable and Clause
Elimination. Niklas Een and Armin Biere SAT 2005: p61—75
- Gilles Audemard, Laurent
Simonm, Predicting Learnt
Clauses Quality in Modern SAT Solvers. IJCAI 2009:
399-404.
- Lecture 4. MaxSat. Readings:
- MiniMaxSat: A New
Weighted Max-SAT Solver. Federico Heras, Javier Larrosa, and Albert Oliveras.
- Postponing
Optimization to Speed Up MAXSAT Solving. Jessica Davies
and Fahiem Bacchus.
- Maximum Satisfiability Using
Core-Guided MAXSAT Resolution. Nina Narodytska and Fahiem
Bacchus.
- 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.
- Lecture 6. QBF. Readings:
- Solving QBF
with Counterexample Guided Refinement by Mikolas Janota, William
Klieber, Joao Marques-Silva and Edmund Clarke
- CAQE: A Certifying QBF Solver
by Markus N. Rabe and Leander Tentrup.
- Incremental Determinization
by Markus N. Rabe and Sanjit A. Seshia.
- Lecture
7. #SAT. Also slides by
Kuldeep Meel on a recent approach to approximate model
counting. (Original slides are here).
Readings:
- Preprocessing
for Propositional Model Counting by Jean-Marie Lagniez and
Pierre Marquis, AAAI-2014
- 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.
- Counting-Based
Reliability Estimation for Power-Transmission Grids. by
Leonardo Duenas-Osorio, Kuldeep S. Meel, Roger Paredes, and
Moshe Y. Vardi. AAAI-2017.
Assignments
- Assignment 2. Out March 14 due April 4th.
- Assignment 1. Out Feb 8th due
March 2nd.
- 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.
- MiniSat home page.
- SAT Encodings of the At-Most-k
Constraint by Alan Frisch and Paul Giannaros