Presentation
Engineering an Efficient Preprocessor for Model Counting
DescriptionGiven a formula F, the problem of model counting is to compute the number of solutions (also known as models) of F. Over the past decade, model counting has emerged as key building block of quantitative reasoning in design automation and artificial intelligence. Given the wide ranging applications, scalability remains the major challenge in the development of model counters. Motivated by the observation that the formula simplification can dramatically impact the performance of the state of the art exact model counters, we design a new state of the art preprocessor, Puura, that relies on tight integration of techniques. The design of Puura is motivated from our observation that it is often beneficial to employ preprocessing techniques whose overhead may be prohibitive for the task of SAT solving but not for model counting: accordingly, we rely on a specifically tailored SAT solver design for redundancy detection, sampling-boosted backbone detection, as well as storing of redundancy information for the purposes of improving propagation within top-down model counters. Our detailed empirical evaluation demonstrates that Puura achieves significant performance improvements over prior model counting preprocessors in terms of instance-size reductions achieved as well as the runtime improvements of the downstream model counters.
Event Type
Research Manuscript
TimeThursday, June 2711:15am - 11:30am PDT
Location3004, 3rd Floor
EDA
Design Verification and Validation