AAAI-07 Tutorial Beyond Traditional SAT Reasoning: QBF, Model Counting, and Solution Sampling Ashish Sabharwal and Bart Selman [ Information | Slides | Description | Syllabus | Speakers ]

The goal of this tutorial is to discuss the basics of and the state of the art in three important problems that extend beyond traditional Boolean satisfiability (SAT) algorithms, namely, Quantified Boolean Formula reasoning, counting the number of models (solutions) of a problem, and near-uniformly sampling from the set of solutions. All three of these problems present fascinating challenges and pose new research questions relevant to anyone working on or interested in SAT methods.

This tutorial will serve a twofold purpose: (a) provide students and researchers new to this area a basic understanding of the problems and the current techniques used to solve them, and (b) outline for those already familiar with SAT solvers the key challenges and bottlenecks involved in transitioning from SAT to problems beyond SAT.

General Information

Tutorial Material

Download: tutorial slides, 4-per-page handouts.

Also see our recent survey of satisfiability solvers (draft pdf) to appear in the Handbook of Knowledge Representation, Elsevier, editors Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter.

Description

Since the early 1990's, algorithms for the Boolean satisfiability problem (SAT solvers) have made a very visible impact on the state of the art in automated reasoning, especially in application areas such as planning, scheduling, and verification. By slowly but steadily incorporating new techniques and features, modern SAT solvers have been made to scale to problems with over a million propositional variables and many more constraints. While SAT methodologies still present interesting and challenging research questions, this tutorial will address three problems that go beyond SAT and will lie at the heart of the next generation automated reasoning systems. These are, Quantified Boolean Formula (QBF) reasoning, counting the number of models (solutions) of a problem, and near-uniformly sampling from the set of solutions. Efficient algorithms for these problems will have a significant impact on many application areas that are inherently beyond SAT, such as adversarial and contingency planning, unbounded model checking, and probabilistic reasoning. The tutorial will also discuss some of these applications.

These three problems --- QBF reasoning, model counting, and solution sampling --- can be solved, in principle and to some extent in practice, by extending the two most successful frameworks for SAT algorithms, namely, DPLL and local search. This tutorial will describe how this is done in the present-day QBF solvers, model counters, and solution samplers. It will also discuss some interesting issues that arise when extending SAT-based techniques to these harder problems. For instance, all three of these problems require the solver to somehow be cognizant of all solutions in the search space, thereby reducing the effectiveness and relevance of commonly used SAT heuristics designed for quickly zooming in on a single solution. We will address such issues, the theoretical hardness of these problems (PSPACE- and #P-completeness), the resulting scalability challenge, and some promising recent techniques that trade off precision with efficiency (in a controlled manner).

Prerequisite Knowledge: This tutorial will be accessible to anyone with an understanding of basic backtrack search and Boolean formulas. Familiarity with techniques used in SAT solvers will be helpful but not essential. No prior knowledge of the three problems (QBF, counting, sampling) will be assumed.

Syllabus

• Background on SAT solvers
  • Problem description, complexity (NP-complete)
  • DPLL-based methods, clause learning, restarts
  • Local search techniques
  
  
• Quantified Boolean Formula (QBF) reasoning
  • Problem description, complexity (PSPACE-complete)
  • Applications, specifically adversarial reasoning and formal verification
  • DPLL-based methods (focus on cube-learning and quantification-aware propagation)
  • Other methods for solving QBF
  • Irrelevant search space issues in QBF
  • Viewing QBF problems as 2-player games; Dual CNF-DNF encodings
  
  
• Model Counting
  • Problem description, complexity (#P-complete)
  • Applications, specifically Bayesian inference
  • DPLL-based methods (focus on complete search and component caching)
  • An XOR-streamlining technique for providing bounds on the model count
  • Exploiting sampling procedures for counting
  
  
• Solution Sampling
  • Problem description, complexity (#P-hard)
  • Applications, specifically in combining logical and probabilistic reasoning
  • Local search techniques (SAT-based methods, general MCMC methods)
  • An XOR-streamlining technique for unbiased sampling
  
  

Speaker Bio

Ashish Sabharwal is a postdoctoral associate in computer science at Cornell University. He received his Ph.D. from the University of Washington in 2005. He has (co)authored over 20 publications, including two that received best paper awards. His research interests include artificial intelligence, automated reasoning, and theoretical computer science, with recent focus on SAT, QBF, and CP.

Bart Selman is a professor of computer science at Cornell University. He was previously at AT&T Bell Laboratories. His research interests include reasoning, planning, knowledge representation, and connections to statistical physics. He has (co)authored over 100 publications, including six best paper awards. He has received the Cornell Miles Excellence in Teaching Award, the Cornell Outstanding Educator Award, an NSF Career Award, and a Sloan Research Fellowship. He is a Fellow of AAAI and of AAAS.

Acknowledgments: This tutorial was funded in part by DARPA.