On the Satisfaction Probability of k-CNF Formulas

Author Till Tantau

Thumbnail PDF


  • Filesize: 0.88 MB
  • 27 pages

Document Identifiers

Author Details

Till Tantau
  • Institute for Theoretical Computer Science, Universität zu Lübeck, Germany

Cite AsGet BibTex

Till Tantau. On the Satisfaction Probability of k-CNF Formulas. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


The satisfaction probability σ(ϕ) := Pr_{β:vars(ϕ) → {0,1}}[β ⊧ ϕ] of a propositional formula ϕ is the likelihood that a random assignment β makes the formula true. We study the complexity of the problem kSAT-PROB_{> δ} = {ϕ is a kCNF formula ∣ σ(ϕ) > δ} for fixed k and δ. While 3SAT-PROB_{> 0} = 3SAT is NP-complete and SAT-PROB}_{> 1/2} is PP-complete, Akmal and Williams recently showed 3SAT-PROB_{> 1/2} ∈ P and 4SAT-PROB_{> 1/2} ∈ NP-complete; but the methods used to prove these striking results stay silent about, say, 4SAT-PROB_{> 3/4}, leaving the computational complexity of kSAT-PROB_{> δ} open for most k and δ. In the present paper we give a complete characterization in the form of a trichotomy: kSAT-PROB_{> δ} lies in AC⁰, is NL-complete, or is NP-complete; and given k and δ we can decide which of the three applies. The proof of the trichotomy hinges on a new order-theoretic insight: Every set of kCNF formulas contains a formula of maximal satisfaction probability. This deceptively simple result allows us to (1) kernelize kSAT-PROB_{≥ δ}, (2) show that the variables of the kernel form a strong backdoor set when the trichotomy states membership in AC⁰ or NL, and (3) prove a locality property by which for every kCNF formula ϕ we have σ(ϕ) ≥ δ iff σ(ψ) ≥ δ for every fixed-size subset ψ of ϕ’s clauses. The locality property will allow us to prove a conjecture of Akmal and Williams: The majority-of-majority satisfaction problem for kCNFS lies in P for all k.

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
  • Satisfaction probability
  • majority it{k}-sat
  • kernelization
  • well orderings
  • locality


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Shyan Akmal and Ryan Williams. majority-3sat (and related problems) in polynomial time. Technical Report abs/2107.02748, Cornell University, 2021. URL: http://arxiv.org/abs/2107.02748.
  2. Shyan Akmal and Ryan Williams. majority-3sat (and related problems) in polynomial time. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS), pages 1033-1043, 2022. Citations and page references in the main text refer to the technical report version [Shyan Akmal and Ryan Williams, 2021] of this paper. URL: https://doi.org/10.1109/FOCS52979.2021.00103.
  3. Max Bannach, Christoph Stockhusen, and Till Tantau. Fast parallel fixed-parameter algorithms via color coding. In 10th International Symposium on Parameterized and Exact Computation, IPEC 2015, volume 43 of LIPIcs, pages 224-235. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  4. Max Bannach and Till Tantau. Computing kernels in parallel: Lower and upper bounds. In 13th International Symposium on Parameterized and Exact Computation, IPEC 2018, volume 115 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  5. Max Bannach and Till Tantau. Computing hitting set kernels by AC⁰-circuits. Theory Comput. Syst., 64(3):374-399, 2020. Google Scholar
  6. Arthur Choi, Yexiang Xue, and Adnan Darwiche. Same-decision probability: A confidence measure for threshold-based decisions. International Journal of Approximate Reasoning, 53(9):1415-1428, 2012. URL: https://doi.org/10.1016/j.ijar.2012.04.005.
  7. Stephen A. Cook. The complexity of theorem-proving procedures. In Conference Record of the Third Annual ACM Symposium on Theory of Computing, pages 151-158, Shaker Heights, Ohio, 1971. Google Scholar
  8. P. Erdős and R. Rado. Intersection theorems for systems of sets. Journal of the London Mathematical Society, 1(1):85-90, 1960. Google Scholar
  9. Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. Springer, 2006. URL: https://doi.org/10.1007/3-540-29953-X.
  10. John T. Gill. Computational complexity of probabilistic turing machines. In Proceedings of the Sixth Annual ACM Symposium on Theory of Computing, STOC '74, pages 91-95, New York, NY, USA, 1974. Association for Computing Machinery. URL: https://doi.org/10.1145/800119.803889.
  11. Thomas Jech. Set Theory: The Third Millennium Edition. Springer, 2003. Google Scholar
  12. Umut Oztok, Arthur Choi, and Adnan Darwiche. Solving pppp-complete problems using knowledge compilation. In Proceedings of the Fifteenth International Conference on Principles of Knowledge Representation and Reasoning, KR'16, pages 94-103. AAAI Press, 2016. Google Scholar
  13. Janos Simon. On Some Central Problems in Computational Complexity. PhD thesis, Cornell University, January 1975. Google Scholar
  14. Till Tantau. On the satisfaction probability of kcnf formulas. Technical Report abs/2201.08895, Cornell University, 2022. URL: http://arxiv.org/abs/2201.08895.
  15. Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput., 8(3):410-421, 1979. URL: https://doi.org/10.1137/0208032.
  16. René van Bevern. Towards optimal and expressive kernelization for d-hitting set. Algorithmica, 70(1):129-147, September 2014. URL: https://doi.org/10.1007/s00453-013-9774-3.
  17. Ryan Williams. Personal communication, 2021. Google Scholar
  18. Ryan Williams, Carla P. Gomes, and Bart Selman. Backdoors to typical case complexity. In Proceedings of the 18th International Joint Conference on Artificial Intelligence, IJCAI'03, pages 1173-1178, San Francisco, CA, USA, 2003. Morgan Kaufmann Publishers Inc. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail