• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Phase Transition Behavior in Knowledge Compilation.
Rahul Gupta, Subhajit Roy and Kuldeep S. Meel.
In Proceedings of International Conference on Constraint Programming (CP), September 2020.
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.
@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.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21