• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Panini: An Efficient and Flexible Knowledge Compiler.
Yong Lai, Kuldeep S. Meel and Roland H. C. Yap.
In Proceedings of International Conference on Computer-Aided Verification (CAV), pp. 92–105, July 2025.
Knowledge compilation concerns with the compilation of representation languages to target languages supporting a wide range of tractable operations arising from diverse areas of computer science. Tractable target compilation languages are usually achieved by restrictions on the internal nodes of the NNF. In this paper, we propose a new representation language CCDD, which introduces new restrictions on conjunction nodes to capture equivalent literals. We show that CCDD supports two key queries, model counting and uniform samping, in polytime. We present algorithms and a compiler to compile propositional formulas expressed in CNF into CCDD. Experiments over a large set of benchmarks show that our compilation times are better with smaller representation than state-of-art Decision-DNNF, SDD and OBDD[AND] compilers. We apply our techniques to model counting and uniform sampling, and develop model counter and uniform sampler on CNF. Our empirical evaluation demonstrates the following significant improvements: our model counter can solve 885 instances while the prior state of the art solved only 843 instances, representing an improvement of 43 instances; and our uniform sampler can solve 780 instances while the prior state of the art solved only 648 instances, representing an improvement of 132 instances.
@inproceedings{LMY25,
title={Panini: An Efficient and Flexible Knowledge Compiler},
author={Lai, Yong and Meel, Kuldeep S. and Yap, Roland H. C.},
booktitle=CAV,
pages={92--105},
year={2025},
month=jul,
bib2html_rescat={Counting, Knowledge Compilation},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf={https://arxiv.org/pdf/2202.10025},
abstract={
Knowledge compilation concerns with the compilation of representation
languages to target languages supporting a wide range of tractable
operations arising from diverse areas of computer science. Tractable target
compilation languages are usually achieved by restrictions on the internal
nodes of the NNF. In this paper, we propose a new representation language
CCDD, which introduces new restrictions on conjunction nodes to capture
equivalent literals. We show that CCDD supports two key queries, model
counting and uniform samping, in polytime. We present algorithms and a
compiler to compile propositional formulas expressed in CNF into CCDD.
Experiments over a large set of benchmarks show that our compilation times
are better with smaller representation than state-of-art Decision-DNNF, SDD
and OBDD[AND] compilers. We apply our techniques to model counting and
uniform sampling, and develop model counter and uniform sampler on CNF. Our
empirical evaluation demonstrates the following significant improvements:
our model counter can solve 885 instances while the prior state of the art
solved only 843 instances, representing an improvement of 43 instances; and
our uniform sampler can solve 780 instances while the prior state of the art
solved only 648 instances, representing an improvement of 132 instances.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21