Armin Biere, Steffen Hölldobler, Sibylle Möhle,
"An Abstract Dual Propositional Model Counter"
, in Steffen Hölldobler, Andrey Malikov, Christoph Wernhard: Proc. Young Scientist's Intl. Workshop on Trends in Information Processing (YSIP2'17), Serie CEUR Workshop Proceedings, Vol. 1837, CEUR, Seite(n) 17-26, 5-2017
An Abstract Dual Propositional Model Counter
Sprache des Titels:
Proc. Young Scientist's Intl. Workshop on Trends in Information Processing (YSIP2'17)
Various real-world problems can be formulated as the task of counting the models of a propositional formula. This problem, also called #SAT, is therefore of practical relevance. We present a formal framework describing a novel approach based on considering the formula in question together with its negation. This method enables us to close search branches earlier. We formalize a non-dual variant and argue that our framework is sound.