Dualizing Projected Model Counting

Beschreibung

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.

Zeitraum	07 Nov. 2018
Ereignistitel	30th International Conference on Tools with Artificial Intelligence,
Veranstaltungstyp	Konferenz
Ort	GriechenlandAuf Karte anzeigen