The past decade has witnessed a surge of interest in practical techniques forprojected model counting . Despite significant advancements, performance scaling remains the Achilles’ heel of this field . Inapplications such as verification of binarized neural networks, quantification of information flow, reliability of power grids etc., a good upper bound of the projected model count often suffices . We show that in several such cases, we can identify a set of variables, called upper bound support (UBS), that is notnecessarily a subset of the projection set . UBS-based projected counting can solve many problem instances that arebeyond the reach of the state-of-the-art projected model counter, we find. Based on extensive experiments, we . find that UBS is more efficient than independent support-based projection counting, while .yielding bounds of very high quality. Theoretically, a UBS can be exponentially smaller than the smallest independentsupport. Our experiments show that even otherwise, UBS, can be more efficient. It can be less efficient than other projections, and yet counting models projected on UBS’s ‘UBS” can solve ‘many problem instances

Author(s) : Jiong Yang, Supratik Chakraborty, Kuldeep S. Meel

Links : PDF - Abstract

Code :

Keywords : ubs - projected - counting - model - based -

Leave a Reply

Your email address will not be published. Required fields are marked *