Many real-world computational problems require a search through an exponentially large space of potential solutions. Examples of such problems can be found in a diverse range of areas, for example, in hardware and software design and verification, planning and scheduling, and artificial intelligence (AI). Many such problems can be translated into a common representation, called the Boolean Satisfiability (SAT) formulation. This formulation consists of a set of Boolean (True/False) variables and logical constraints among these variables. The challenge is to find an assignment to the variables such that all constraints are satisfied. In recent years, we have seen tremendous progress in the development of SAT solvers, which search for satisfying assignments. Current SAT solvers handle problem instances with over one million variables and several millions of constraints. An intriguing research question is whether the advances in SAT technology can be exploited for other key reasoning tasks central to AI.
This project considers three such tasks: (1) quantified Boolean reasoning, key in multi-agent reasoning and reasoning in adversarial settings, (2) counting of the number of satisfying assignments, which has many applications in probabilistic inference, and (3) sampling from the set of satisfying assignments, which is closely related to model counting. The broader impact of the proposal will be the design and development of efficient solvers for quantified Boolean formulas (QBF) and algorithms for model counting and sampling applicable to a wide range of users working in areas as diverse as verification, planning, adversarial reasoning, and probabilistic reasoning.
