• 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 Sun Apr 14, 2024 11:15:51