Recently, a number of non-uniform random satisfiability models have been proposed that are closer to practical satisfiability problems in some characteristics. In contrast to uniform random Boolean formulas, scale-free formulas have a variable occurrence distribution that follows a power law. It has been conjectured that such a distribution is a more accurate model for some industrial instances than the uniform random model. Though it seems that there is already an awareness of a threshold phenomenon in such models, there is still a complete picture lacking. In contrast to the uniform model, the critical density threshold does not lie at a single point, but instead exhibits a functional dependency on the power-law exponent. For scale-free formulas with clauses of length \(k = 2\), we give a lower bound on the phase transition threshold as a function of the scaling parameter. We also perform computational studies that suggest our bound is tight and investigate the critical density for formulas with higher clause lengths. Similar to the uniform model, on formulas with \(k 3\), we find that the phase transition regime corresponds to a set of formulas that are difficult to solve by backtracking search.
%0 Conference Paper
%1 DBLP:conf/aaai/0001KRS17
%A Friedrich, Tobias
%A Krohmer, Anton
%A Rothenberger, Ralf
%A Sutton, Andrew M.
%B Association for the Advancement of Artificial Intelligence (AAAI)
%D 2017
%I AAAI Press
%K testing typo3
%P 3893-3899
%T Phase Transitions for Scale-Free SAT Formulas
%X Recently, a number of non-uniform random satisfiability models have been proposed that are closer to practical satisfiability problems in some characteristics. In contrast to uniform random Boolean formulas, scale-free formulas have a variable occurrence distribution that follows a power law. It has been conjectured that such a distribution is a more accurate model for some industrial instances than the uniform random model. Though it seems that there is already an awareness of a threshold phenomenon in such models, there is still a complete picture lacking. In contrast to the uniform model, the critical density threshold does not lie at a single point, but instead exhibits a functional dependency on the power-law exponent. For scale-free formulas with clauses of length \(k = 2\), we give a lower bound on the phase transition threshold as a function of the scaling parameter. We also perform computational studies that suggest our bound is tight and investigate the critical density for formulas with higher clause lengths. Similar to the uniform model, on formulas with \(k 3\), we find that the phase transition regime corresponds to a set of formulas that are difficult to solve by backtracking search.
@inproceedings{DBLP:conf/aaai/0001KRS17,
abstract = {Recently, a number of non-uniform random satisfiability models have been proposed that are closer to practical satisfiability problems in some characteristics. In contrast to uniform random Boolean formulas, scale-free formulas have a variable occurrence distribution that follows a power law. It has been conjectured that such a distribution is a more accurate model for some industrial instances than the uniform random model. Though it seems that there is already an awareness of a threshold phenomenon in such models, there is still a complete picture lacking. In contrast to the uniform model, the critical density threshold does not lie at a single point, but instead exhibits a functional dependency on the power-law exponent. For scale-free formulas with clauses of length \(k = 2\), we give a lower bound on the phase transition threshold as a function of the scaling parameter. We also perform computational studies that suggest our bound is tight and investigate the critical density for formulas with higher clause lengths. Similar to the uniform model, on formulas with \(k \geq 3\), we find that the phase transition regime corresponds to a set of formulas that are difficult to solve by backtracking search.},
added-at = {2017-09-19T19:31:34.000+0200},
author = {Friedrich, Tobias and Krohmer, Anton and Rothenberger, Ralf and Sutton, Andrew M.},
biburl = {https://www.bibsonomy.org/bibtex/254a98bdc88615625cb97cfaa7482af5f/typo3tester},
booktitle = {Association for the Advancement of Artificial Intelligence (AAAI)},
crossref = {DBLP:conf/aaai/2017},
interhash = {f6e5308755096bf06e5daf430209a4a1},
intrahash = {54a98bdc88615625cb97cfaa7482af5f},
keywords = {testing typo3},
pages = {3893-3899},
publisher = {AAAI Press},
timestamp = {2017-09-19T19:31:34.000+0200},
title = {Phase Transitions for Scale-Free SAT Formulas},
year = 2017
}