Abstract
Knowledge compilation is the process of algorithmically transforming a given formula to a form that permits certain queries to be answered in time polynomial in the size of the compiled form. Well-known knowledge compiled forms for propositional formulas include OBDDs, FBDDs, DNNF, d-DNNF, SDDs etc. Each of these allow polynomial-time satisfiability checking and beyond (including existential quantification, synthesis and even model-counting in some cases). For purposes of quantification and (functional) synthesis however, all of the above forms enjoy properties that are much stronger than required. In this talk, we will discuss knowledge compilation for quantification and synthesis, and show that a significantly weaker (exponentially more succinct) form suffices. We will discuss some compilation algorithms, and point to future directions for knowledge compilation for problems beyond NP.