In many recent applications of model counting not all
variables are relevant for a specific problem. For instance redundant
variables are added during formula transformation. In projected model
counting these redundant variables are ignored by projecting models onto
relevant variables. Inspired by dual propagation which has its origin in
solving quantified Boolean formulae and jointly works on both the
original formula and its negation, we present a novel calculus for dual
projected model counting. It allows to capture existing techniques such
as blocking clauses, chronological as well as non-chronological
backtracking, but also introduces new concepts including discounting and
dual conflict analysis to obtain partial models. Experiments demonstrate
the benefit of our approach.
Forschungs-