Solving Non-uniform Planted and Filtered Random SAT Formulas Greedily

Tobias Friedrich, Frank Neumann, Ralf Rothenberger, Andrew M. Sutton

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

Abstract

Recently, there has been an interest in studying non-uniform random k-satisfiability (k-SAT) models in order to address the non-uniformity of formulas arising from real-world applications. While uniform random k-SAT has been extensively studied from both a theoretical and experimental perspective, understanding the algorithmic complexity of heterogeneous distributions is still an open challenge. When a sufficiently dense formula is guaranteed to be satisfiable by conditioning or a planted assignment, it is well-known that uniform random k-SAT is easy on average. We generalize this result to the broad class of non-uniform random k-SAT models that are characterized only by an ensemble of distributions over variables with a mild balancing condition. This balancing condition rules out extremely skewed distributions in which nearly half the variables occur less frequently than a small constant fraction of the most frequent variables, but generalizes recently studied non-uniform k-SAT distributions such as power-law and geometric formulas. We show that for all formulas generated from this model of at least logarithmic densities, a simple greedy algorithm can find a solution with high probability. As a side result we show that the total variation distance between planted and filtered (conditioned on satisfiability) models is o(1) once the planted model produces formulas with a unique solution with probability 1 - o(1 ). This holds for all random k-SAT models where the signs of variables are drawn uniformly and independently at random.

Original languageEnglish (US)
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2021 - 24th International Conference, 2021, Proceedings
EditorsChu-Min Li, Felip Manyà
PublisherSpringer Science and Business Media Deutschland GmbH
Pages188-206
Number of pages19
ISBN (Print)9783030802226
DOIs
StatePublished - Jul 2 2021
Event24th International Conference on Theory and Applications of Satisfiability Testing, SAT 2021 - Barcelona, Spain
Duration: Jul 5 2021Jul 9 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12831 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Conference on Theory and Applications of Satisfiability Testing, SAT 2021
Country/TerritorySpain
CityBarcelona
Period7/5/217/9/21

Bibliographical note

Funding Information:
Keywords: Random k-SAT · Planted k-SAT · Non-uniform variable distribution · Greedy algorithm · Local search Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – 416061626.

Publisher Copyright:
© 2021, Springer Nature Switzerland AG.

Keywords

  • Greedy algorithm
  • Local search
  • Non-uniform variable distribution
  • Planted k-SAT
  • Random k-SAT

Fingerprint

Dive into the research topics of 'Solving Non-uniform Planted and Filtered Random SAT Formulas Greedily'. Together they form a unique fingerprint.

Cite this