On the Satisfaction Probabilities of $k$-CNF Formulas
Abstract
The satisfaction probability Pr[] := Pr of a propositional formula is the likelihood that a random assignment makes the formula true. We study the complexity of the problem SAT-Pr = { is a CNF formula | Pr[] > p} for fixed and . While 3SAT-Pr = 3SAT is NP-complete and SAT-Pr is PP-complete, Akmal and Williams recently showed that 3SAT-Pr lies in P and 4SAT-Pr is NP-complete; but the methods used to prove these striking results stay silent about, say, 4SAT-Pr, leaving the computational complexity of SAT-Pr open for most and . In the present paper we give a complete characterization in the form of a trichotomy: SAT-Pr lies in AC, is NL-complete, or is NP-complete. The proof of the trichotomy hinges on a new order-theoretic insight: Every set of CNF formulas contains a formula of maximum satisfaction probability. This deceptively simple statement allows us to (1) kernelize SAT-Pr for the joint parameters and , (2) show that the variables of the kernel form a backdoor set when the trichotomy states membership in AC or NL, and (3) prove locality properties for CNF formulas , by which Pr[] < implies that Pr[] < holds already for a subset of 's clauses whose size depends only on and , and Pr[] = implies for some CNF formula whose size once more depends only on and .
Keywords
Cite
@article{arxiv.2201.08895,
title = {On the Satisfaction Probabilities of $k$-CNF Formulas},
author = {Till Tantau},
journal= {arXiv preprint arXiv:2201.08895},
year = {2024}
}
Comments
47 pages, version updated after the presentation of the results at the CCC 2022 conference and after further reviewing