More Web Proxy on the site http://driver.im/

research-article

PPSZ for k ≥ 5: More Is Better

Author:

Dominik SchederAuthors Info & Claims

ACM Transactions on Computation Theory (TOCT), Volume 11, Issue 4

Article No.: 25, Pages 1 - 22

https://doi.org/10.1145/3349613

Published: 12 September 2019 Publication History

Abstract

We show that for k ≥ 5, the PPSZ algorithm for k-SAT runs exponentially faster if there is an exponential number of satisfying assignments. More precisely, we show that for every k≥ 5, there is a strictly increasing function f: [0,1] → R with f(0) = 0 that has the following property. If F is a k-CNF formula over n variables and |sat(F)| = 2^{δ n} solutions, then PPSZ finds a satisfying assignment with probability at least 2^{−c_k n −o(n) + f(δ) n}. Here, 2^{−c_k n −o(n)} is the success probability proved by Paturi et al. [11] for k-CNF formulas with a unique satisfying assignment.

Our proof rests on a combinatorial lemma: given a set S ⊆ { 0,1} ⁿ, we can partition { 0,1} ⁿ into subcubes such that each subcube B contains exactly one element of S. Such a partition B induces a distribution on itself, via Pr [B] = |B| / 2ⁿ for each B ∈ B. We are interested in partitions that induce a distribution of high entropy. We show that, in a certain sense, the worst case (min_{S: |S| = s} max_B H(B)) is achieved if S is a Hamming ball. This lemma implies that every set S of exponential size allows a partition of linear entropy. This in turn leads to an exponential improvement of the success probability of PPSZ.

References

[1]

Sven Baumer and Rainer Schuler. 2003. Improving a probabilistic 3-SAT algorithm by dynamic search and independent clause pairs. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT’03) (Lecture Notes in Computer Science), Enrico Giunchiglia and Armando Tacchella (Eds.), vol. 2919. Springer, 150--161.

[2]

Béla Bollobás. 1986. Combinatorics: Set Systems, Hypergraphs, Families of Vectors, and Combinatorial Probability. Cambridge University Press, New York, NY.

Digital Library

[3]

Chris Calabro, Russell Impagliazzo, Valentine Kabanets, and Ramamohan Paturi. 2008. The complexity of unique k-SAT: An isolation lemma for k-CNFs. J. Comput. Syst. Sci. 74, 3 (2008), 386--393.

Digital Library

[4]

Timon Hertli. 2011. 3-SAT faster and simpler—Unique-SAT bounds for PPSZ hold in general. In Proceedings of the IEEE 52nd Annual Symposium on Foundations of Computer Science (FOCS’11). IEEE, Los Alamitos, CA, 277--284.

Digital Library

[5]

Timon Hertli. 2014. Breaking the PPSZ barrier for unique 3-SAT. In Proceedings of the 41st International Colloquium on Automata, Languages, and Programming (ICALP’14) (Lecture Notes in Computer Science), Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias (Eds.), vol. 8572. Springer, 600--611.

[6]

Timon Hertli, Robin A. Moser, and Dominik Scheder. 2011. Improving PPSZ for 3-SAT using critical variables. In Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS’11). 237--248.

[7]

Thomas Hofmeister, Uwe Schöning, Rainer Schuler, and Osamu Watanabe. 2002. A probabilistic 3-SAT algorithm further improved. In Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS’02) (Lecture Notes in Computer Science), Helmut Alt and Afonso Ferreira (Eds.), vol. 2285. Springer, 192--202.

Digital Library

[8]

Kazuo Iwama, Kazuhisa Seto, Tadashi Takai, and Suguru Tamaki. 2010. Improved randomized algorithms for 3-SAT. In Proceedings of the 21st International Symposium on Algorithms and Computation (ISAAC’10) (Lecture Notes in Computer Science), Otfried Cheong, Kyung-Yong Chwa, and Kunsoo Park (Eds.), vol. 6506. Springer, 73--84.

[9]

Kazuo Iwama and Suguru Tamaki. 2004. Improved upper bounds for 3-SAT. In Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms. ACM, New York, 328--329.

Digital Library

[10]

Ramamohan Paturi. {n.d.}. Personal communication.

[11]

Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane. 2005. An improved exponential-time algorithm for k-SAT. J. ACM 52, 3 (2005), 337--364 (electronic).

Digital Library

[12]

Ramamohan Paturi, Pavel Pudlák, and Francis Zane. 1999. Satisfiability coding lemma. Chicago J. Theoret. Comput. Sci. (1999).

[13]

Daniel Rolf. 2006. Improved bound for the PPSZ/Schöning-Algorithm for 3-SAT. J. Satisfiabil., Boolean Model. Comput. 1 (2006), 111--122.

[14]

N. Sauer. 1972. On the density of families of sets. J. Combinat. Theory, Ser. A 13, 1 (1972), 145--147.

[15]

Dominik Scheder and John P. Steinberger. 2017. PPSZ for general k-SAT—Making Hertli’s analysis simpler and 3-SAT faster. In Proceedings of the 32nd Computational Complexity Conference (CCC’17) (LIPIcs), Ryan O’Donnell (Ed.), vol. 79. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 9:1--9:15.

Digital Library

[16]

Uwe Schöning. 1999. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In Proceedings of the 40th Annual Symposium on Foundations of Computer Science. IEEE, Los Alamitos, CA, 410--414.

Digital Library

[17]

Saharon Shelah. 1972. A combinatorial problem: Stability and order for models and theories in infinitary languages. Pacific J. Math. 41, 1 (1972), 247--261.

Cited By

Scheder DSteinberger J(2024)PPSZ for General k-SAT and CSP—Making Hertli’s Analysis Simpler and 3-SAT FasterComputational Complexity10.1007/s00037-024-00259-y33:2Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1007/s00037-024-00259-y
Scheder DTalebanfard NAceto L(2020)Super strong ETH is true for PPSZ with small resolution widthProceedings of the 35th Computational Complexity Conference10.4230/LIPIcs.CCC.2020.3(1-12)Online publication date: 28-Jul-2020
https://dl.acm.org/doi/10.4230/LIPIcs.CCC.2020.3

Index Terms

PPSZ for k ≥ 5: More Is Better
1. Theory of computation
  1. Design and analysis of algorithms
    1. Parameterized complexity and exact algorithms

Recommendations

PPSZ for general k-SAT: making Hertli's analysis simpler and 3-SAT faster
CCC '17: Proceedings of the 32nd Computational Complexity Conference

In this paper, we achieve three goals. First, we simplify Hertli's 2011 analysis [1] for input formulas with multiple satisfying assignments. Second, we show a "translation result": if you improve PPSZ for k-CNF formulas with a unique satisfying ...
PPSZ for General k-SAT and CSP—Making Hertli’s Analysis Simpler and 3-SAT Faster
Abstract
The currently fastest known algorithm for k-SAT is PPSZ, named after its inventors (Paturi et al. in J ACM 52(3):337-364, 2005. ). Analyzing its running time is much easier for input formulas with a unique ...
Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts
DAC '09: Proceedings of the 46th Annual Design Automation Conference

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computation Theory

ACM Transactions on Computation Theory Volume 11, Issue 4

December 2019

252 pages

ISSN:1942-3454

EISSN:1942-3462

DOI:10.1145/3331049

Editor:
Venkatesan Guruswami
Carnegie Mellon University, USA

Issue’s Table of Contents

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 September 2019

Accepted: 01 May 2019

Revised: 01 April 2019

Received: 01 July 2018

Published in TOCT Volume 11, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

National Science Foundation of China

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
106
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 05 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Scheder DSteinberger J(2024)PPSZ for General k-SAT and CSP—Making Hertli’s Analysis Simpler and 3-SAT FasterComputational Complexity10.1007/s00037-024-00259-y33:2Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1007/s00037-024-00259-y
Scheder DTalebanfard NAceto L(2020)Super strong ETH is true for PPSZ with small resolution widthProceedings of the 35th Computational Complexity Conference10.4230/LIPIcs.CCC.2020.3(1-12)Online publication date: 28-Jul-2020
https://dl.acm.org/doi/10.4230/LIPIcs.CCC.2020.3

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View Issue’s Table of Contents