Sibylle Möhle, Armin Biere,
"Dualizing Projected Model Counting"
: Proc. 30th Intl. Conf. on Tools with Artificial Intelligence (ICTAI'18), IEEE Computer Society, 2018
Dualizing Projected Model Counting
Sprache des Titels:
Proc. 30th Intl. Conf. on Tools with Artificial Intelligence (ICTAI'18)
In many recent applications of model counting not all variables are relevant for a speci?c problem. For instance redundantvariablesareaddedduringformulatransformation.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 quanti?ed Boolean formulae and jointly works on both the original formula and its negation, we present a novel calculus for dual projected model counting.Itallowstocaptureexistingtechniquessuchasblocking clauses, chronological as well as non-chronological backtracking, but also introduces new concepts including discounting and dual con?ict analysis to obtain partial models. Experiments demonstrate the bene?t of our approach.