Description

The field of Automated Reasoning is concerned with the following objectives:

the formal representation of systems and phenomena using logic;
the automatic derivation of logical conclusions based on these representations; and
the application of these results to problems in science and engineering.

Automated Reasoning is at the intersection of Artificial Intelligence, Mathematical Logic, and Algorithmic Design & Analysis.
It has a wide range of applications, including but not limited to: diagnosis, planning, design, formal verification, and reliability analysis.

The focus of this course is on the theory and practice of automated reasoning using propositional (Boolean) logic.

In the first part of the course, we will provide a detailed exposition of the syntax and semantics of propositional logic and then move on to state-of-the-art algorithms for automated reasoning. In particular, we will focus on satisfiability (SAT) engines which are based on both exhaustive-search and stochastic-search methods. We will then study a variety of tractable logical representations, which have been prevalent in computer science and engineering, including those based on Binary Decision Diagrams (BDDs), negation normal forms, prime implicates and clausal forms. We will also study algorithms for compiling logical representations from one form to another, and algorithms for answering sophisticated logical queries such as logical entailment, equivalence testing, model counting and logical projection.

In the second part of the course, we will focus on applications of automated reasoning, which include diagnosis and testing, planning, belief revision, formal verification, reliability analysis, and the factoring of probabilistic models. For each of these applications, we will provide a formalization using logic; then study representational considerations that arise in the context of these applications; and finally detail solutions based on the representations and reasoning algorithms developed in the first part.

Prerequisites

No AI background is required, but mathematical and algorithmic maturity is expected.

Requirements

Class participation.
Midterm.
Final (may be replaced by a project with instructor consent).

Tentative Schedule

Week 1: Introduction. Quantified propositional logic & Boolean functions. Classical logic representations.
Week 2: Resolution.
Week 3: Satisfiability (SAT) and counting engines.
Week 4: A road map of tractable represenations in propositional logic. Tractable representations based on negation normal forms (NNFs).
Week 5: Decomposability and Determinism. Compilation algorithms.
Week 6: Midterm. Tractable representations based on binary decision diagrams (BDDs).
Week 7: Tractable representations based on prime implicants/implicates and Horn clauses. Complexity results and succinctness comparisons between different representations.
Week 8: Diagnosis and testing.
Week 9: Formal verification & planning.
Week 10: Probabilistic reasoning.

Readings:

Complete SAT (directed resolution):

Rish & Dechter. "Resolution versus Search: Two Strategies for SAT." In "Journal of Automated Reasoning", special issue on SAT, Volume 24, Issue 1/2, pp. 225-275, Januray, 2000.

Complete SAT (dpll):

Berkmin SAT solver.
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an Efficient SAT Solver, 39th Design Automation Conference, Las Vegas, June 2001.
Silva and Sakallah. GRASP-A new search algorithm for satisfiability.
L. Zhang and S. Malik. The Quest for Efficient Boolean Satisfiability Solvers. Proceedings of 8th International Conference on Computer Aided Deduction (CADE 2002) and also in Proceedings of 14th Conference on Computer Aided Verification (CAV2002), Copenhagen, Denmark, July 2002.
L. Zhang, C. Madigan, M. Moskewicz, S. Malik. Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. Proceedings of ICCAD 2001, San Jose, CA, Nov. 2001.
Kuntz & Pradhan. Recursive learning: A new implication technique for efficient solutions to CAD Problems. IEEE Transactions on computer-aided design of integrated circuits and systems. Vol 13. No 9. Pages 1143-1158. 1994.

Branching heuristics:

LI & Anbulagan. Heuristics based on unit propagation for satisfiability problems, IJCAI97.
Williams, Gomes, Selman. Backdoors to typical case complexity. IJCAI03
J. Wang. Branching rules for propositional satisfiability test. DIMACS series in Discrete Mathematics and Theoretical Computer Science. Vol 35, 1997.

Incomplete SAT:

Selman, Kautz, & Cohen. Local search strategies for satisfiability testing.

SAT generation:

Cook & Mitchell. Finding Hard Instances of the Satisfiability Problem: A Survey. In "Satisfiability Problem: Theory and Applications", DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997.

Model counting:

Birnbaum & Lozinskii. The good old Davis-Putnam procedure helps counting models, JAIR Volume 10, pages 457-477, 1999.
Gomes, Subharwal, Selman. Model counting: A new strategy for obtaining good bounds. AAAI06.
Bayardo and Pehoushek. Counting models using connected components. AAAI'2000

Knowledge Compilation:

Darwiche & Marquis. A knowledge compilation map. JAIR 02.
Darwiche. Decomposable negation normal form. JACM 01.
Darwiche. On the tractable counting of theory models. JANCL 01.
Darwiche. New advances in compiling CNF to DNNF. ECAI04.
Darwiche. A Compiler for deterministic decomposable negation normal form. AAAI'02.
Adnan Darwiche and Jinbo Huang. Testing Equivalence Probabilistically. Technical Report D-123.

Binay decision diagrams:

Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol. c-35, no.8, Aug. 1986.
Drechsler and Sieling. Binary decision diagrams in theory and practice. Software Tools for Technology Transfer 3, 112-136.
Gergov and Meinel. Efficient Boolean Manipulation with OBDDs can be Extended to FBDDs. Tech report.
Huang and Darwiche. Using DPLL for efficient OBDD construction. SAT04. Slides.
Blum, Chandra and Wegman. Equivalence of free Boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters. Vol 10, No 2, pp. 80-82, March 18, 1980.
Symbolic SAT. Slides.
Huang and Darwiche. DPLL with a trace: From satisfiability to knowledge compilation. Slides.
Pan and Vardi. Symbolic Techniques in Satisfiability Solving (Full version of SAT'04 paper with G. Pan).

Prime Implicants/Theory approximation:

Selman and Kautz. Knowledge compilation and theory approximation.

Diagnosis and testing:

Johan de Kleer, Alan K. Mackworth, Raymond Reiter: Characterizing Diagnoses and Systems. Artificial Intelligence 56(2-3): 197-222 (1992).
Darwiche. Model-based diagnosis under real-word constraints. AI Magazine.
T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Transactions on computer-aided design. Vol 11, No 1, 4-15, 1992.

Planning:

Rintanen and Hoffmann, An overview of recent algorithms for AI planning, Künstliche Intelligenz, (2):5-11, May 2001.
Kautz & Selman. Planning as satisfiability.

Probabilistic Reasoning:

slides

Useful Links

Lecture Notes

Homework

Useful Books

Algorithms and Data Structures in VLSI Design, C. Meinel and T. Theobald. Springer.

Model Checking, E. Clarke, O. Grumberg and D. Peled. MIT Press.

Logical Foundations of Artificial Intelligence, M. Genesereth and N. Nilsson.