• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Engineering an Efficient Preprocessor for Model Counting.
Mate Soos, and Kuldeep S. Meel.
In Proceedings of Design Automation Conference (DAC), June 2024.
Given a formula F , the problem of model counting is to computethe number of solutions (also known as models) of F. Over thepast decade, model counting has emerged as key building block ofquantitative reasoning in design automation and artificial intelligence.Given the wide-ranging applications, scalability remains themajor challenge. Motivated by the observation that the formulasimplification can dramatically impact the performance of the stateof-the-art exact model counters, we design a new state-of-the-artpreprocessor, Arjun2, that relies on tight integration of techniques. The design of Arjun2 is motivated from our observation that it is oftenbeneficial to employ preprocessing techniques whose overheadmay be prohibitive for the task of SAT solving but not for modelcounting: accordingly, we rely on a specifically tailored SAT solverdesign for redundancy detection, sampling-boosted backbone detection,as well as storing of redundancy information for the purposesof improving propagation within top-down model counters. Our detailed empirical evaluation demonstrates that Arjun2 achieves significant performance improvements over prior model countingpreprocessors in terms of instance-size reductions achieved as wellas the runtime improvements of the downstream model counters.
@inproceedings{SM24,
title={Engineering an Efficient Preprocessor for Model Counting},
author={Soos, Mate and Meel, Kuldeep S.},
abstract={
Given a formula F , the problem of model counting is to computethe number of solutions
(also known as models) of F. Over thepast decade, model counting has emerged as key building
block ofquantitative reasoning in design automation and artificial intelligence.Given the wide-ranging applications,
scalability remains themajor challenge. Motivated by the observation that the formulasimplification can dramatically impact the performance of the stateof-the-art exact model counters, we design a new state-of-the-artpreprocessor, Arjun2, that relies on tight integration of techniques.
The design of Arjun2 is motivated from our observation that it is oftenbeneficial to employ preprocessing
techniques whose overheadmay be prohibitive for the task of SAT solving but not for modelcounting: accordingly,
we rely on a specifically tailored SAT solverdesign for redundancy detection, sampling-boosted backbone detection,as well as
storing of redundancy information for the purposesof improving propagation within top-down model counters.
Our detailed empirical evaluation demonstrates that Arjun2 achieves significant performance improvements over prior model countingpreprocessors in terms of instance-size reductions achieved as wellas the runtime improvements of the downstream model counters.
},
month=jun,
year={2024},
booktitle=DAC,
bib2html_pubtype={Refereed Conference},
bib2html_rescat={Counting, Solver Engineering},
bib2html_dl_pdf={../Papers/dac24-sm.pdf},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51