Phase transitions for scale-free SAT formulas

Tobias Friedrich, Anton Krohmer, Ralf Rothenberger, Andrew M. Sutton

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

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 ≥ 3, we find that the phase transition regime corresponds to a set of formulas that are difficult to solve by backtracking search.

Original languageEnglish (US)
Title of host publication31st AAAI Conference on Artificial Intelligence, AAAI 2017
PublisherAAAI press
Pages3893-3899
Number of pages7
StatePublished - Jan 1 2017
Event31st AAAI Conference on Artificial Intelligence, AAAI 2017 - San Francisco, United States
Duration: Feb 4 2017Feb 10 2017

Other

Other31st AAAI Conference on Artificial Intelligence, AAAI 2017
CountryUnited States
CitySan Francisco
Period2/4/172/10/17

Fingerprint Dive into the research topics of 'Phase transitions for scale-free SAT formulas'. Together they form a unique fingerprint.

Cite this