As a submission to the Beyond NP workshop at AAAI 2016, we amended the 2012 Canadian AI paper that describes DSHARP [1]. Unfortunately, due to copyright regulations with the publisher Springer, this submission can not be distributed publicly. However, the additional text is reproduced below, and a slightly extended version of the original Canadian AI paper submitted at a prior workshop can be found here.
Relying on the trace of a complete DPLL based solver is the prevailing technique for CNF → d-DNNF compilers, used by both DSHARP and C2D [2]. The DPLL trace has been leveraged for proving bounds on model counting, such as the work of Beame et al. [3]. It has also been used to good effect for proving theoretical results about the worst-case size complexity of the d-DNNF representation [4].
Knowledge compilers (including the DSHARP software presented in this paper) have played a role as subcomponents in larger systems. One example is in the SAT-based analysis of quantification information flow programs, where efficient methods for conditioned model counting using d-DNNF were exploited [5]. Another example is the Probabilistic Logic Programming framework, ProbLog [6]. Here, the model counters were used to provide probabilistic inference for targeted queries compiled from a given logic program.
Finally, since the original publication of this work in 2012 by Muise et al., the DSHARP software has been extended in a variety of ways. Most notably, the software has been extended to do model counting with the assumption of stable model semantics [7], as well as extended to do projected model counting and projected knowledge compilation [8].
For stable model counting, every model represented by the compiled theory must be stable: a notion in logic programming that stipulates that the truth of atoms cannot be self supporting given the logic program’s rules [9]. To accommodate for stable models, DSHARP was modified to include an internal propagator that rules out any model deemed not stable. Subsequently, clauses are learned to rule out the unstable models and the final compiled d-DNNF theory represents all stable models.
The problem of projected model counting (respectively projected knowledge compilation) is to count the number of models (resp. produce the d-DNNF) for the Boolean theory after projecting away a subset of the variables. Intuitively, a model for the projected theory exists if the same setting of variables corresponds to at least one model of the full theory. DSHARP was modified in a variety of ways to achieve projected model counting and knowledge compilation. These included (1) dedicated variable ordering heuristics to focus on the projected variables; (2) advanced back-tracking to avoid recomputing the same projected model; and (3) a re-determinization method to convert a DNNF theory back into d-DNNF.