MAJORITY-3SAT (and Related Problems) in Polynomial Time
- LRM

Majority-SAT is the problem of determining whether an input -variable formula in conjunctive normal form (CNF) has at least satisfying assignments. Majority-SAT and related problems have been studied extensively in various AI communities interested in the complexity of probabilistic planning and inference. Although Majority-SAT has been known to be PP-complete for over 40 years, the complexity of a natural variant has remained open: Majority-SAT, where the input CNF formula is restricted to have clause width at most . We prove that for every , Majority-SAT is in P. In fact, for any positive integer and rational with bounded denominator, we give an algorithm that can determine whether a given -CNF has at least satisfying assignments, in deterministic linear time (whereas the previous best-known algorithm ran in exponential time). Our algorithms have interesting positive implications for counting complexity and the complexity of inference, significantly reducing the known complexities of related problems such as E-MAJ-SAT and MAJ-MAJ-SAT. At the heart of our approach is an efficient method for solving threshold counting problems by extracting sunflowers found in the corresponding set system of a -CNF. We also show that the tractability of Majority-SAT is somewhat fragile. For the closely related GtMajority-SAT problem (where we ask whether a given formula has greater than satisfying assignments) which is known to be PP-complete, we show that GtMajority-SAT is in P for , but becomes NP-complete for . These results are counterintuitive, because the ``natural'' classifications of these problems would have been PP-completeness, and because there is a stark difference in the complexity of GtMajority-SAT and Majority-SAT for all .
View on arXiv