@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.
  },
}