The Satisfiability Threshold for Non-Uniform Random 2-SAT
Propositional satisfiability (SAT) is one of the most fundamental problems in computer science. Its worst-case hardness lies at the core of computational complexity theory, for example in the form of NP-hardness and the (Strong) Exponential Time Hypothesis. In practice however, SAT instances can often be solved efficiently. This contradicting behavior has spawned interest in the average-case analysis of SAT and has triggered the development of sophisticated rigorous and non-rigorous techniques for analyzing random structures.
Despite a long line of research and substantial progress, most theoretical work on random SAT assumes a uniform distribution on the variables. In contrast, real-world instances often exhibit large fluctuations in variable occurrence. This can be modeled by a non-uniform distribution of the variables, which can result in distributions closer to industrial SAT instances.
We study satisfiability thresholds of non-uniform random 2-SAT with n variables and m clauses and with an arbitrary probability distribution (p_i)_{i in[n]} with p_1 >=slant p_2 >=slant ... >=slant p_n>0 over the n variables. We show for p_{1}^2=Theta (sum_{i=1}^n p_i^2) that the asymptotic satisfiability threshold is at {m=Theta ((1-{sum_{i=1}^n p_i^2})/(p_1 * (sum_{i=2}^n p_i^2)^{1/2}))} and that it is coarse. For p_{1}^2=o (sum_{i=1}^n p_i^2) we show that there is a sharp satisfiability threshold at m=(sum_{i=1}^n p_i^2)^{-1}. This result generalizes the seminal works by Chvatal and Reed [FOCS 1992] and by Goerdt [JCSS 1996].
random SAT
satisfiability threshold
sharpness
non-uniform distribution
2-SAT
Theory of computation~Generating random combinatorial structures
61:1-61:14
Track A: Algorithms, Complexity and Games
This paper is partially funded by the project Skalenfreie Erfüllbarkeit (project no. 416061626) of the German Research Foundation (DFG).
A full version of the paper is available at https://arxiv.org/abs/1904.02027.
Tobias
Friedrich
Tobias Friedrich
Algorithm Engineering Group, Hasso Plattner Institute, University of Potsdam, Germany
https://orcid.org/0000-0003-0076-6308
Ralf
Rothenberger
Ralf Rothenberger
Algorithm Engineering Group, Hasso Plattner Institute, University of Potsdam, Germany
https://orcid.org/0000-0002-4133-2437
10.4230/LIPIcs.ICALP.2019.61
Dimitris Achlioptas, Lefteris M. Kirousis, Evangelos Kranakis, and Danny Krizanc. Rigorous results for random (2+p)-SAT. Theor. Comput. Sci., 265(1-2):109-129, 2001.
Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, and Jordi Levy. The Fractal Dimension of SAT Formulas. In 7th Intl. Joint Conf. Automated Reasoning (IJCAR), pages 107-121, 2014.
Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, and Jordi Levy. On the Classification of Industrial SAT Families. In 18th Intl. Conf. of the Catalan Association for Artificial Intelligence (CCIA), pages 163-172, 2015.
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. On the Structure of Industrial SAT Instances. In 15th Intl. Conf. Principles and Practice of Constraint Programming (CP), pages 127-141, 2009.
Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Towards Industrial-Like Random SAT Instances. In 21st Intl. Joint Conf. Artificial Intelligence (IJCAI), pages 387-392, 2009.
Carlos Ansótegui, Jesús Giráldez-Cru, and Jordi Levy. The Community Structure of SAT Formulas. In 15th Intl. Conf. Theory and Applications of Satisfiability Testing (SAT), pages 410-423, 2012.
Victor Bapst and Amin Coja-Oghlan. The Condensation Phase Transition in the Regular k-SAT Model. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques, APPROX/RANDOM 2016, pages 22:1-22:18, 2016.
Yacine Boufkhad, Olivier Dubois, Yannet Interian, and Bart Selman. Regular Random k-SAT: Properties of Balanced Formulas. J. Autom. Reasoning, 35(1-3):181-200, 2005.
Milan Bradonjic and Will Perkins. On Sharp Thresholds in Random Geometric Graphs. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques, APPROX/RANDOM 2014, pages 500-514, 2014.
Karl Bringmann. Why Walking the Dog Takes Time: Frechet Distance Has No Strongly Subquadratic Algorithms Unless SETH Fails. In 55th Symp. Foundations of Computer Science (FOCS), pages 661-670, 2014.
Václav Chvatal and Bruce Reed. Mick gets some (the odds are on his side). In 33rd Symp. Foundations of Computer Science (FOCS), pages 620-627, 1992.
Amin Coja-Oghlan. The Asymptotic k-SAT Threshold. In 46th Symp. Theory of Computing (STOC), pages 804-813, 2014.
Amin Coja-Oghlan and Konstantinos Panagiotou. The asymptotic k-SAT threshold. Advances in Mathematics, 288:985-1068, 2016.
Amin Coja-Oghlan and Nick Wormald. The Number of Satisfying Assignments of Random Regular k-SAT Formulas. Combinatorics, Probability and Computing, 27(4):496–530, 2018.
Stephen A. Cook. The Complexity of Theorem-Proving Procedures. In 3rd Symp. Theory of Computing (STOC), pages 151-158, 1971.
Colin Cooper, Alan Frieze, and Gregory Sorkin. Random 2SAT with Prescribed Literal Degrees. Algorithmica, 48:249-265, July 2007.
Marek Cygan, Jesper Nederlof, Marcin Pilipczuk, Michal Pilipczuk, Johan M. M. van Rooij, and Jakub Onufry Wojtaszczyk. Solving Connectivity Problems Parameterized by Treewidth in Single Exponential Time. In 52nd Symp. Foundations of Computer Science (FOCS), pages 150-159, 2011.
Josep Díaz, Lefteris M. Kirousis, Dieter Mitsche, and Xavier Pérez-Giménez. On the satisfiability threshold of formulas with three literals per clause. Theoretical Computer Science, 410(30-32):2920-2934, 2009.
Jian Ding, Allan Sly, and Nike Sun. Proof of the Satisfiability Conjecture for Large K. In 47th Symp. Theory of Computing (STOC), pages 59-68, 2015.
Tobias Friedrich, Anton Krohmer, Ralf Rothenberger, Thomas Sauerwald, and Andrew M. Sutton. Bounds on the Satisfiability Threshold for Power Law Distributed Random SAT. In 25th European Symposium on Algorithms (ESA), pages 37:1-37:15, 2017.
Tobias Friedrich, Anton Krohmer, Ralf Rothenberger, and Andrew M. Sutton. Phase Transitions for Scale-Free SAT Formulas. In 31st Conf. Artificial Intelligence (AAAI), pages 3893-3899, 2017.
Tobias Friedrich and Ralf Rothenberger. Sharpness of the Satisfiability Threshold for Non-uniform Random k-SAT. In 21st Intl. Conf. Theory and Applications of Satisfiability Testing (SAT), pages 273-291, 2018.
Jesús Giráldez-Cru and Jordi Levy. A Modularity-Based Random SAT Instances Generator. In 24 thIntl. Joint Conf. Artificial Intelligence (IJCAI), pages 1952-1958, 2015.
Andreas Goerdt. A Threshold for Unsatisfiability. J. Comput. Syst. Sci., 53(3):469-486, 1996.
Mohammad Taghi Hajiaghayi and Gregory B. Sorkin. The Satisfiability Threshold of Random 3-SAT is at Least 3.52. Technical Report RC22942, IBM, October 2003.
Russell Impagliazzo and Ramamohan Paturi. On the Complexity of k-SAT. J. Comput. Syst. Sci., 62(2):367-375, 2001.
Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which Problems Have Strongly Exponential Complexity? In 39th Symp. Foundations of Computer Science (FOCS), pages 653-663, 1998.
Alexis C. Kaporis, Lefteris M. Kirousis, and Efthimios G. Lalas. The probabilistic analysis of a greedy satisfiability algorithm. Random Struct. Algorithms, 28(4):444-480, 2006.
Richard M. Karp. Reducibility Among Combinatorial Problems. In Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York., pages 85-103, 1972.
Leonid A. Levin. Universal sorting problems. Problems of Information Transmission, 9:265-266, 1973.
Jordi Levy. Percolation and Phase Transition in SAT. CoRR, abs/1708.06805, 2017. URL: http://arxiv.org/abs/1708.06805.
http://arxiv.org/abs/1708.06805
Marc Mézard, Giorgio Parisi, and Riccardo Zecchina. Analytic and algorithmic solution of random satisfiability problems. Science, 297(5582):812-815, 2002.
David G. Mitchell, Bart Selman, and Hector J. Levesque. Hard and Easy Distributions of SAT Problems. In 10th Conf. Artificial Intelligence (AAAI), pages 459-465, 1992.
Rémi Monasson and Riccardo Zecchina. Statistical mechanics of the random K-satisfiability model. Phys. Rev. E, 56:1357-1370, August 1997.
Rémi Monasson, Riccardo Zecchina, Scott Kirkpatric, Bart Selman, and Lidror Troyansky. Phase transition and search cost in the 2+ p-sat problem. 4th Workshop on Physics and Computation, Boston, MA, 1996., 1996.
Rémi Monasson, Riccardo Zecchina, Scott Kirkpatrick, Bart Selman, and Lidror Troyansky. 2+p-SAT: Relation of typical-case complexity to the nature of the phase transition. Random Struct. Algorithms, 15(3-4):414-435, 1999.
Nathan Mull, Daniel J. Fremont, and Sanjit A. Seshia. On the Hardness of SAT with Community Structure. In 19th Intl. Conf. Theory and Applications of Satisfiability Testing (SAT), pages 141-159, 2016.
Vishwambhar Rathi, Erik Aurell, Lars K. Rasmussen, and Mikael Skoglund. Bounds on Threshold of Regular Random k-SAT. In 13th Intl. Conf. Theory and Applications of Satisfiability Testing (SAT), pages 264-277, 2010.
Tobias Friedrich and Ralf Rothenberger
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode