@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@inproceedings{GRM20b,
  title={Phase Transition Behavior in Knowledge Compilation},
  author={Gupta, Rahul and Roy, Subhajit and Meel, Kuldeep S.},
  bib2html_dl_pdf={https://arxiv.org/abs/2007.10400},
  booktitle=CP,
  month=sep,
  year={2020},
  bib2html_rescat={Phase Transitions},
  bib2html_pubtype={Refereed Conference},
  abstract={The success of SAT solvers has led to development of algorithmic paradigms for problems beyond NP such as knowledge compilation, which seeks to compile proposition theory into succinct and tractable representations. The study of phase transition behaviour in SAT has been subjected to intense theoretical and empirical investigations, and has led to deeper understanding and algorithmic improvements of modern SAT solvers. Motivated by the prior studies of phase transition in SAT, we seek to study the behaviour of size and compile-time behaviour for random k-CNF formulas.
The primary contribution of this paper is a rigorous empirical study and analysis of the size and runtime behavior for different knowledge compilation forms (and their corresponding compilation algorithms): d-DNNFs, SDDs and OBDDs. We employ instances generated from random k-CNF model with varying generation parameters to empirically reason about the expected and median behavior of size and compilation-time for these languages. A significant novel contribution of our work is the identification of a new control parameter, called solution density, defined as the ratio of the log of number of satisfying assignments to number of variables.},
}