Abstract
We consider the "compilation" of a Boolean formula into a circuit, a notion introduced by Darwiche and Marquis; our compilation targets are OBDDs, FBDDs, and Decision-DNNFs. We are interested in the case when the Boolean formula is the provenance of an FO sentence over a finite domain of size n. The question becomes: for a fixed FO sentence, what is the size (as a function of n) of the optimal circuit representing the provenance formula? When F is restricted to a universally quantified, positive FO sentence, and the compilation target consists of OBDDs, then we prove a dichotomy: the optimal size is either polynomial in n, or is exponentially large. When the compilation target consists of FBDDs or Decision-DNNFs, then a full dichotomy remains open, but we prove an important limitation for these families of circuits: there exists FO sentences whose provenance formulas admit PTIME model counting, yet any circuit has exponential size. Therefore, these types of circuits are insufficient to do model counting in PTIME for all FO sentences for which a PTIME model counting algorithm is known. An open problem is to identify a class of circuits for Boolean formulas such that every FO sentence with tractable model counting can be compiled into a circuit in that family, of size at most polynomial in the domain.
Joint work with Paul Beame, Abhay Jha, Jerry Li, Sudeepa Roy.