# MAJORITY-3SAT (and Related Problems) in Polynomial Time ††thanks: Supported
by NSF CCF-1909429 and NSF CCF-1741615.

Shyan Akmal
MIT
<EMAIL_ADDRESS>Ryan Williams
MIT
<EMAIL_ADDRESS>This work was done while the author was visiting the Simons
Institute for the Theory of Computing, participating in the _Theoretical
Foundations of Computer Systems_ and _Satisfiability: Theory, Practice, and
Beyond_ programs.

###### Abstract

Majority-SAT (a.k.a. MAJ-SAT) is the problem of determining whether an input
$n$-variable formula in conjunctive normal form (CNF) has at least $2^{n-1}$
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-$k$SAT, where the input CNF formula is restricted to
have clause width at most $k$.

We prove that for every $k$, Majority-$k$SAT is in P; in fact, the problem can
be solved in linear time (whereas the previous best-known algorithm ran in
exponential time). More generally, for any positive integer $k$ and constant
$\rho\in(0,1)$ with bounded denominator, we give an algorithm that can
determine whether a given $k$-CNF has at least $\rho\cdot 2^{n}$ satisfying
assignments, in deterministic linear time. We find these results surprising,
as many analogous problems which are hard for CNF formulas remain hard when
restricted to $3$-CNFs. 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-$k$SAT and
MAJ-MAJ-$k$SAT. Our results immediately extend to arbitrary Boolean CSPs with
constraints of arity $k$. At the heart of our approach is an efficient method
for solving threshold counting problems by extracting and analyzing various
sunflowers found in the corresponding set system of a $k$-CNF.

Exploring the implications of our results, we find that the tractability of
Majority-$k$SAT is somewhat fragile, in intriguing ways. For the closely
related GtMajority-SAT problem (where we ask whether a given formula has
_greater than_ $2^{n-1}$ satisfying assignments) which is also known to be
${\mathsf{PP}}$-complete, we show that GtMajority-$k$SAT is in P for $k\leq
3$, but becomes NP-complete for $k\geq 4$. We also show that for Majority-SAT
on $k$-CNFs with one additional clause of arbitrary width, the problem is PP-
complete for $k\geq 4$, is NP-hard for $k=3$, and remains in P for $k=2$.
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-$k$SAT and Majority-$k$SAT for all
$k\geq 4$.

##  1 Introduction

The complexity of $\\#$SAT, the problem of counting satisfying assignments to
propositional formulas (a.k.a. “model counting” in the AI and SAT literature),
has been intensely studied for decades. The pioneering work of Valiant [Val79]
showed that $\\#$SAT is $\\#{\mathsf{P}}$-complete already for 2-CNF formulas.

Of course, $\\#$SAT (and any other $\\#{\mathsf{P}}$ problem) is a function
problem: up to $n+1$ bits need to be output on a given $n$-variable formula. A
natural question is: how efficiently can output bits of the $\\#$SAT function
be computed? Obvious choices are the _low-order bit_ , which corresponds to
the $\oplus\mathsf{P}$-complete PARITY-SAT problem, and the _higher-order
bits_. For CNF formulas, the highest-order bit of $\\#$SAT corresponds to the
case where the $\\#$SAT value is $2^{n}$, which is trivial for CNF
formulas.111The only $n$-variable CNFs with $2^{n}$ satisfying assignments are
those with no clauses. Of course, when the formula is DNF, the high-order bit
problem is $\mathsf{coNP}$-complete. When the value is less than $2^{n}$ and
$\\#$SAT outputs $n$ bits, the high-order bit corresponds to MAJORITY-SAT, the
problem of determining whether $\\#\text{SAT}(F)\geq 2^{n-1}$. It is more
common to think of it as a probability threshold problem: given a formula $F$,
is $\Pr_{a}[F(a)=1]\geq 1/2$? Sometimes MAJORITY-SAT is phrased as determining
whether or not $\Pr_{a}[F(a)=1]>1/2$; we will call this version GtMAJORITY-SAT
to avoid confusion. Over CNF formulas (and more expressive Boolean
representations), there is no essential difference between the two
problems.222See Section 2 for a discussion.

MAJORITY-SAT (and GtMAJORITY-SAT) are the primary subjects of this paper. Gill
[Gil74] and Simon [Sim75] introduced these problems along with the class
${\mathsf{PP}}$, which consists of decision problems computing “high-order
bits” of a $\\#P$ function. They proved that MAJORITY-SAT on CNF formulas is
${\mathsf{PP}}$-complete, and that
$\\#{\mathsf{P}}\subseteq\mathsf{P}^{{\mathsf{PP}}}$, showing that determining
higher-order bits of a general $\\#{\mathsf{P}}$ function is as hard as
computing the entire function.

The known proofs of ${\mathsf{PP}}$-hardness for MAJORITY-SAT reduce to CNF
formulas having clauses of arbitrarily large width. This raises the very
natural question of whether MAJORITY-SAT remains hard over CNFs with fixed-
width clauses. Intuition suggests that MAJORITY-$k$SAT should remain
${\mathsf{PP}}$-hard for $k\geq 3$, by analogy with the $\mathsf{NP}$-hardness
of 3SAT, the ${\mathsf{PSPACE}}$-hardness of Quantified 3SAT [Sto76], the
$\oplus\mathsf{P}$-hardness of PARITY-3SAT333This follows from the fact that
there is a parsimonious reduction from SAT to 3-SAT [Sim75]., the
$\Pi_{2}\mathsf{P}$-hardness of $\Pi_{2}$-$3$SAT [SM73], and so on. Beyond the
SAT problem, it is often true that the hardness of a problem can be preserved
for “bounded width/degree” versions of the problem: for instance, the
$\mathsf{NP}$-hardness of $3$-coloring holds even for graphs of degree at most
$4$ [GJ79], and the $\\#{\mathsf{P}}$-hardness of counting perfect matchings
in graphs holds even for graphs of degree at most $3$ [DL92]. Indeed, the more
general problem: _given a $3$-CNF $F$ and an integer $k\geq 0$, determine if
$\\#SAT(F)\geq 2^{k}$_ can readily be proved ${\mathsf{PP}}$-complete.
However, the same argument cannot be used to show that MAJORITY-SAT is
${\mathsf{PP}}$-complete for 3-CNF $F$.444The proof of
${\mathsf{PP}}$-completeness (of the more general problem) follows from two
facts: (a) the version of the problem for CNF formulas is
${\mathsf{PP}}$-complete, by Gill and Simon, and (b) the reduction from CNF-
SAT to 3SAT preserves the number of solutions. This proof cannot be used to
show that determining $\\#SAT(F)\geq 2^{n-1}$ is ${\mathsf{PP}}$-complete for
$3$-CNF $F$, because the Cook-Levin reduction introduces many new variables
(the variable $n$ increases when going from CNF-SAT to 3SAT, thereby changing
the target number of satisfying assignments).

Due to these subtleties, there has been significant confusion in the
literature about the complexity of MAJORITY-$k$SAT, with several works
asserting intractability for MAJORITY-3SAT and its variants, while others
observing that the complexity of the problem remained open at the time
[Mun00a, Mun00b, BDK01, KG05, BDK07, GHM08, KG09, TF10, PLMZ11, Kwi11, FGL12,
KdC15a, KdC15b, MDCC15, CDdB16, CM18, BDPR19, BDPR20].555Even the second
author is guilty of being confused: see the first comment at
https://cstheory.stackexchange.com/questions/36660/status-of-pp-completeness-
of-maj3sat. This is a critical issue, as MAJORITY-SAT and its variants have
been at the foundation of many reductions regarding the complexity of
probabilistic planning, Bayesian inference, and maximum a posteriori problems
in restricted settings, which are of great interest to various communities
within AI. The true complexity of MAJORITY-$k$SAT (and related problems) has
remained a central open question for these communities.

###  1.1 Our Results

Somewhat surprisingly, we show that MAJORITY-SAT over $k$-CNFs is in fact
easy. In fact, for any constant $\rho\in(0,1)$, we can efficiently determine
for a given $k$-CNF $F$ whether $\Pr_{a\in\\{0,1\\}^{n}}[F(a)=1]\geq\rho$ or
not.

######  Theorem 1.1.

For every constant rational $\rho\in(0,1)$ and every constant $k\geq 2$, there
is a deterministic linear-time algorithm that given a $k$-CNF $F$ determines
whether or not $\\#SAT(F)\geq\rho\cdot 2^{n}$.

To our knowledge, the previous best-known algorithm for this problem ran in
$2^{n-\Theta(n/k)}$ time, by running the best-known algorithm for $\\#k$SAT
[IMP12, CW21]. Of course, Theorem 1.1 does not mean that $\\#\mathsf{P}$
functions can be computed in polynomial time; rather, it shows that lower-
order bits of $\\#k$SAT are the more difficult ones666Indeed in some sense,
“middle bits” are ${\mathsf{PP}}$-hard: Bailey, Dalmau, and Koliatis [BDK01,
BDK07] showed 20 years ago that for all integers $t\geq 2$, determining
whether $\\#\text{SAT}(F)\geq 2^{n/t}$ (for 3-CNF $F$) is
${\mathsf{PP}}$-complete. (Corollary 5.7 in Section 5.1 formally describes how
to use our algorithm to compute the high-order bits of $\\#k$SAT in polynomial
time). Even the lowest-order bit of $\\#k$SAT is evidently harder: for every
$k\geq 2$, PARITY-$k$SAT is known to be $\oplus\mathsf{P}$-complete [Val06],
so (by Toda’s theorem [Tod91]) the low-order bit of $\\#k$SAT cannot be
computed in ${\mathsf{BPP}}$ unless $\mathsf{NP}=\mathsf{RP}$.

#### Implications for Related Inference Problems.

Given that MAJORITY-$k$SAT turns out to be easy, it is worth exploring whether
related problems in literature are also easy or hard. In the relevant AI
literature on the complexity of Bayesian inference and probabilistic planning,
the following two problems are prominent in proving conditional lower bounds:

> E-MAJ-SAT: _Given $n$, $n^{\prime}$, and a formula $\varphi$ over
> $n+n^{\prime}$ variables, is there a setting to the first $n$ variables of
> $\phi$ such that the majority of assignments to the remaining $n^{\prime}$
> variables are satisfying assignments?_
>
> MAJ-MAJ-SAT: _Given $n$, $n^{\prime}$, and a formula $\varphi$ over
> $n+n^{\prime}$ variables, do a majority of the assignments to the first $n$
> variables of $\varphi$ yield a formula where the majority of assignments to
> the remaining $n^{\prime}$ variables are satisfying?_

These problems may seem esoteric, but E-MAJ-SAT and related problems are used
extensively in the relevant areas of AI, where an environment has inherently
“random” aspects along with variables one can control, and one wants to “plan”
the control variables to maximize the chance that a desired property holds
(e.g. [LGM98, PD04, Dar09]). E-MAJ-SAT has also recently been used to study
the complexity of verifying differential privacy [GNP20].

Similarly, MAJ-MAJ-SAT applies in the context when one wants to know what is
the chance that a random setting of control variables will yield a good chance
that a property holds [CXD12, OCD16].

For general CNF formulas, E-MAJ-SAT is $\mathsf{NP}^{{\mathsf{PP}}}$-complete
[Wag86, Tor91, LGM98] and MAJ-MAJ-SAT is
${\mathsf{PP}}^{{\mathsf{PP}}}$-complete [Wag86, Tor91, AKR+01]: roughly
speaking, these results imply that both problems are essentially intractable,
even assuming oracle access to a $\\#$SAT solver (we give a proof of
completeness for E-MAJ-SAT for $6$-CNFs with one arbitrary-width clause in
Appendix D). There has also been significant confusion about whether
E-MAJ-3SAT (the version restricted to $3$-CNF) is
$\mathsf{NP}^{{\mathsf{PP}}}$-complete or not [KG05, KG09, MDCC15, CDdB16,
BDPR19, BDPR20]. We prove that both E-MAJ-SAT and MAJ-MAJ-SAT dramatically
decrease in complexity over $k$-CNF formulas.

######  Theorem 1.2.

E-MAJ-$2$SAT $\in\mathsf{P}$, and for all $k\geq 3$, E-MAJ-$k$SAT is
$\mathsf{NP}$-complete.

######  Theorem 1.3.

MAJ-MAJ-2SAT $\in\mathsf{P}$.

Even the $\mathsf{NP}$-completeness of E-MAJ-3SAT is good news, in some sense:
Theorem 1.2 suggests that such counting problems could in principle be handled
by SAT solvers, rather than needing $\\#$SAT solvers.

#### Greater-Than MAJORITY-SAT.

The algorithms behind Theorem 1.1 can efficiently determine if the $\\#$SAT
value of a $k$-CNF is _at least_ a given fraction of the satisfying
assignments. Recall the GtMAJORITY-SAT problem is to determine if the $\\#$SAT
value is _greater than_ a given fraction, and that over CNFs, there is no
essential difference between the two problem variants. Another surprise is
that, over $k$-CNFs, there is a difference between these problems for $k\geq
4$: the “greater than” version becomes $\mathsf{NP}$-complete!

######  Theorem 1.4.

For all $k\leq 3$, GtMAJORITY-$k$SAT is in $\mathsf{P}$.

######  Theorem 1.5.

For all $k\geq 4$, GtMAJORITY-$k$SAT is $\mathsf{NP}$-complete.

#### Adding One Long Clause Makes MAJORITY-$\boldsymbol{k}$SAT Hard.

Given the surprisingly low complexity of these threshold counting problems
over $k$-CNF formulas, it is natural to investigate what extensions of
$k$-CNFs suffice in order for the problems to become difficult. This direction
is also important for the considerable collection of results in AI whose
complexity hinges on the difficulty of MAJORITY-SAT and its variants. We show
that adding only _one_ extra clause of arbitrary width is already enough to
make MAJORITY-$k$SAT difficult, for $k\geq 3$.

######  Theorem 1.6.

Deciding MAJORITY-SAT over $k$-CNFs with one extra clause of arbitrary width
is in $\mathsf{P}$ for $k=2$, $\mathsf{NP}$-hard for $k=3$, and
${\mathsf{PP}}$-complete for $k\geq 4$.

This may look preposterous: how could adding only one long clause make
MAJORITY-$3$SAT hard? Couldn’t we simply try all $O(n)$ choices for picking a
literal from the long clause, and reduce the problem to $O(n)$ calls to
MAJORITY-$3$SAT with no long clauses? Apparently not! Remember that
MAJORITY-$3$SAT _only_ decides whether or not the fraction of satisfying
assignments is at least $\rho\in(0,1)$. This information does not help us
determine the number of satisfying assignments to $O(n)$ subformulas
accurately enough to refute the hardness of MAJORITY-$3$SAT with no long
clauses.

###  1.2 Intuition

The ideas behind our algorithms arose from reconsidering the polynomial-time
Turing reduction from $\\#$SAT to MAJORITY-SAT [Gil74, Sim75], in the hopes of
proving that MAJORITY-$3$SAT is hard. The key is to reduce the problem

$\\#\text{SATD}:=\\{(F,s)\mid\\#\text{SAT}(F)\geq s\\}$

to MAJORITY-SAT. From there, one can binary search with $\\#$SATD to determine
$\\#\text{SAT}(F)$. The known reductions from $\\#$SATD to MAJORITY-SAT
require that, given a desired $t\in[0,2^{n}]$, we can efficiently construct a
formula $G_{t}$ on $n$ variables with exactly $t$ satisfying assignments.777A
standard way to do this is to make a formula $G_{t}$ which is true if and only
if its variable assignment, construed as an integer in $[1,2^{n}]$, is at most
$t$. But constructing such a formula requires arbitrary width CNFs. Then,
introducing a new variable $x_{n+1}$, the formula

$H=(x_{n+1}\vee F)\wedge(\neg x_{n+1}\vee G_{t})$

will have $\\#\text{SAT}(H)=\\#\text{SAT}(F)+t$, out of $2^{n+1}$ possible
assignments to $H$. Setting $t=2^{n}-s$, it follows that $\\#\text{SAT}(F)\geq
s$ if and only if $\\#\text{SAT}(H)\geq 2^{n}$, thereby reducing from
$\\#$SATD to MAJORITY-SAT. Observe we can convert $H$ into $k$-CNF, provided
that both $F$ and $G_{t}$ are $(k-1)$-CNF.

However, this reduction fails miserably for $k$-CNF formulas, because for
constant $k$ and large $n$, there are many values $t\in[0,2^{n}]$ for which
_no_ $k$-CNF formula $G_{t}$ has exactly $t$ satisfying assignments (observe
that every $k$-CNF with at least one clause has at most $(1-1/2^{k})\cdot
2^{n}$ satisfying assignments; therefore no such $k$-CNF formulas $G_{t}$
exist, for all $t\in[2^{n}-2^{n-k}-1,2^{n}-1]$). Moreover, every $k$-CNF
containing $d$ disjoint clauses ($d$ clauses sharing no variables) has at most
$(1-1/2^{k})^{d}\cdot 2^{n}$ satisfying assignments. But “most” $k$-CNF
formulas (say, from the typical random $k$-SAT distributions) _will_ have
_large_ disjoint sets of clauses (say, of size $\Omega(n)$). So for “most”
formulas, we can quickly determine that $\\#\text{SAT}(F)<\rho\cdot 2^{n}$ for
constant $\rho>0$, by finding a large enough disjoint clause set.

What remains is a rather structured subset of $k$-CNF formulas. If the maximum
possible size of a disjoint clause set is small, then there is a small set of
variables that “hit” all other clauses (otherwise, the set would not be
maximal). That is, there is a small set of variables that have non-empty
intersection with every clause. This kind of small hitting set can be very
algorithmically useful for solving $\\#$SAT. For example, if $k=2$, then every
assignment to the variables in a small hitting set simplifies the given
formula into a $1$-CNF. In other words, when there is a small hitting set, we
can reduce the computation of $\\#2$SAT to a small number of calls to
$\\#1$SAT, each of which can be solved in polynomial time. This is essentially
how our algorithm for MAJORITY-$2$SAT works.

The situation quickly becomes more technically complicated, as $k$ increases.
When $k=3$, setting all variables in a small hitting set merely simplifies the
formula to a $2$-CNF, but $\\#$SAT is already $\\#\mathsf{P}$-hard for $2$-CNF
formulas. To get around this issue, we consider more generally _sunflowers_
within the $k$-CNF: collections of sets which all share the same pairwise
intersection (called the core).

Sunflowers in a formula can be useful in bounding the fraction of satisfying
assignments. To give a simple example, if the entire formula was a sunflower
with a single literal $\ell$ in its core, then the fraction of satisfying
assignments is at least $1/2$ (because setting $\ell$ true already satisfies
the formula). Our algorithms seek out large sunflowers on disjoint clauses in
$k$-CNF formulas, to get tighter and tighter bounds on the fraction of
satisfying assignments. When a formula does not have many such sunflowers, the
formula is structured enough that we can find a small hitting set of variables
and use the ideas discussed earlier.

#### Intuition for Theorem 1.1.

Here we provide an intuitive idea of how our main algorithm works to determine
whether a $k$-CNF has at least a $\rho$-fraction of satisfying assignments.
Given a Boolean formula $\Phi$ on $n$ variables, let $\Pr[\Phi]$ denote the
probability a uniform random assignment to the variables of $\Phi$ is
satisfying. For a given $k$-CNF $\varphi$, we want to decide whether the
inequality

$\Pr[\varphi]\geq\rho$

holds or not. We will do this by building up a special $(k-2)$-CNF $\psi$ on
the same variable set, where each clause of $\psi$ is contained in a clause of
$\varphi$. We split the probability calculation into

$\Pr[\varphi]=\Pr[\varphi\land\psi]+\Pr[\varphi\land\lnot\psi]$

and use the fact that

$\Pr[\varphi\land\psi]\leq\Pr[\varphi]=\Pr[\varphi\land\psi]+\Pr[\varphi\land\lnot\psi].$
(1)

Intuitively, we will construct $\psi$ in such a way that
$\Pr[\varphi\land\lnot\psi]<{\varepsilon}_{1}$ for an _extremely_ small
${\varepsilon}_{1}>0$, so that it is possible to reduce the problem of
determining $\Pr[\varphi]\geq\rho$ to the problem of determining
$\Pr[\varphi\land\psi]\geq\rho$. In other words, we can reduce THRρ-$k$SAT on
$\varphi$ to THRρ-$k$SAT on $\varphi\land\psi$.

This reduction is helpful because the clauses of $\psi$ are subclauses
appearing frequently in $\varphi$, so the formula $\varphi\land\psi$
simplifies to a smaller formula than $\varphi$. Additionally,
$\varphi\wedge\psi$ has a smaller solution space than $\varphi$, so
intuitively it becomes easier to check if the resulting formula has fewer than
a $\rho$-fraction of satisfying assignments. More precisely, it follows from
(1) that if $\Pr[\varphi\land\psi]\geq\rho$ then $\Pr[\varphi]\geq\rho$ as
well. The more surprising result is that we can construct $\psi$ so that, if
$\Pr[\varphi\land\psi]<\rho$, then we can in fact infer that
$\Pr[\varphi\land\psi]<\rho-{\varepsilon}_{2}$ for some
${\varepsilon}_{2}>{\varepsilon}_{1}$. Hence by (1) we can deduce that
$\Pr[\varphi]<{\varepsilon}_{1}+\rho-{\varepsilon}_{2}<\rho$.

We construct the clauses of $\psi$ by taking cores of large sunflowers in
$\varphi$. Defining what counts as “large” depends on quite a few parameters,
so the analysis becomes rather technical.

###  1.3 Paper Organization

In Section 2, we formally define the problems we are considering, introduce
notation, and discuss more related work.

The proof that MAJORITY-$k$SAT is in $\mathsf{P}$ (Theorem 1.1) is spread
across multiple sections, to enhance readability. In Section 3 we present a
simple algorithm for solving MAJORITY-$2$SAT in linear time, and in Section 4
we extend this algorithm to solve MAJORITY-$3$SAT in linear time. Building on
these preliminary results, in Section 4.3 we use more sophisticated arguments
to show that for any fixed rational $\rho\in(0,1)$ with denominator bounded
above by a constant, we can detect if a 3-CNF on $n$ variables has at least
$\rho 2^{n}$ satisfying assignments in linear time. In Section 5 we extend the
results to $k$-CNFs for any fixed integer $k$, finally proving Theorem 1.1.
Although Section 5 subsumes the main results of the prior sections, we include
the proofs of these simpler cases earlier in order to motivate and highlight
the key ideas in the final algorithm, and make the overall proof more
accessible.

In Section 6 we discuss the applications of our algorithmic results to the
E-MAJ-SAT and MAJ-MAJ-SAT problems. In Section 7.1 we discuss hardness results
for MAJORITY-$k$SAT with one arbitrary width clause, and in Section 7.2 we
discuss GtMAJORITY-$k$SAT and how it differs from MAJORITY-$k$SAT. We conclude
in Section 8 with a discussion of several intriguing open problems.

##  2 Preliminaries

We assume basic familiarity with computational complexity, including concepts
such as ${\mathsf{PP}}$ and $\\#{\mathsf{P}}$ [AB09]. For a formula $F$ on $n$
variables, let $\\#\text{SAT}(F)$ be its number of satisfying assignments as
an integer in $[0,2^{n}]$.

CNF Formulas. A literal is a Boolean variable or its negation, a _clause_ is a
disjunction of literals, and a _CNF formula_ is a conjunction of clauses. The
_width_ of a clause is the number of literals it contains. Given an integer
$w$, a _$w$ -clause_ is just a clause of width $w$. Given a positive integer
$k$, we say a formula is a $k$-CNF if every clause in the formula has width
_at most_ $k$. We stress that we allow our $k$-CNFs to have clauses of length
_up to_ $k$: clauses of width $1,\ldots,k$ are allowed. An empty CNF formula
evaluates to $\top$, meaning it is always true. An empty clause evaluates to
$\bot$, meaning it is always false. Given a CNF formula $\varphi$, we let
$|\varphi|$ denote the size of the formula, which is just the sums of the
widths of all clauses in $\varphi$.

We remark that all of the results in this paper that hold for $k$-CNF formulas
also hold for Boolean constraint satisfaction problems (CSPs), over arbitrary
constraints of arity at most $k$. This is because each constraint of such a
CSP can be converted into an equivalent $k$-CNF over the same variable set.

GtMAJORITY-SAT vs MAJORITY-SAT. Here we briefly describe how to reduce between
these two problems. To reduce from GtMAJORITY-SAT to MAJORITY-SAT given an
$n$-variable formula $F$, introduce $n$ new variables $y_{1},\ldots,y_{n}$ and
map $F$ to $F^{\prime}:=(y_{1}\vee\cdots\vee y_{n})\wedge F$. Then
$\\#\text{SAT}(F)\geq 2^{n-1}+1$ implies
$\\#\text{SAT}(F^{\prime})\geq(2^{n}-1)(2^{n-1}+1)=2^{2n-1}+2^{n}-2^{n-1}-1>2^{2n-1}$
and $\\#\text{SAT}(F)\leq 2^{n-1}$ implies
$\\#\text{SAT}(F^{\prime})\leq(2^{n}-1)2^{n-1}=2^{2n-1}-2^{n-1}<2^{2n-1}$.

To reduce from MAJORITY-SAT to GtMAJORITY-SAT given an $n$-variable $F$,
introduce one new variable $x_{n+1}$, let $G$ be an $n$-variable formula with
precisely $2^{n}-2^{n-1}+1$ satisfying assignments, and set $F^{\prime}:=(\neg
x_{n+1}\vee F)\wedge(x_{n+1}\vee G)$. Then
$\\#\text{SAT}(F^{\prime})=\\#\text{SAT}(F)+2^{n}-2^{n-1}+1$. When
$\\#\text{SAT}(F)\geq 2^{n-1}$, we have $\\#\text{SAT}(F^{\prime})\geq
2^{n}+1$, and when $\\#\text{SAT}(F)\leq 2^{n-1}-1$ we have
$\\#\text{SAT}(F^{\prime})\leq 2^{n}$ (we can increase the gap by increasing
the number of additional variables). Both reductions need unbounded width CNF
formulas.

Threshold SAT. We have already defined the MAJORITY-$k$SAT problem. To discuss
problems of detecting fractions of satisfying assignments at other thresholds
besides $1/2$, we introduce the following problem.

######  Definition 2.1 (Threshold SAT).

For any positive integer $k$ and threshold $\rho\in(0,1)$, the THRρ-$k$SAT
problem is the following task: given a $k$-CNF formula $\varphi$ on $n$
variables, determine if the inequality $\\#\text{SAT}(\varphi)\geq\rho\cdot
2^{n}$ holds.

In our algorithms, we will often make use of the following structures in CNF
formulas.

######  Definition 2.2 (Consistent Literal Set).

Given a set of literals, we say the set is _consistent_ if the set does not
simultaneously include $x$ and $\lnot x$ for any variable $x$.

######  Definition 2.3 (Variable Disjoint Set).

Given a set $S$ of clauses, we say $S$ is a (variable) _disjoint set_ if for
every pair $C,C^{\prime}$ of distinct clauses of $S$, $C$ and $C^{\prime}$
share no variables.

We will also utilize the following simple observations about CNFs formulas.

######  Proposition 2.4.

Let $F$ be a CNF formula on $n$ variables, construed as a set of clauses.
Suppose there is a $\rho\in(0,1)$ and a subset $F^{\prime}$ of the clauses of
$F$ such that $F^{\prime}$ contains $r\leq n$ variables and
$\\#SAT(F^{\prime})\leq\rho\cdot 2^{r}$. Then $\\#SAT(F)\leq\rho\cdot 2^{n}$.

###### Proof.

Note that $F=F^{\prime}\wedge G$, for some formula $G$. Given a fixed
$F^{\prime}$, the number of satisfying assignments to $F$ is maximized when
$G$ is a tautology, having $2^{n}$ satisfying assignments (since $F$ is over
$n$ variables, we can take $G=(x_{1}\vee\neg
x_{1})\wedge\cdots\wedge(x_{n}\vee\neg x_{n})$). Even in such a case,
$\\#\text{SAT}(F)\leq\\#\text{SAT}(F^{\prime})\cdot 2^{n-r}\leq\rho\cdot
2^{n}$. ∎

######  Proposition 2.5.

Given a 1-CNF formula $F$ (i.e. $F$ is a conjunction of literals), the number
of satisfying assignments to $F$ can be computed in linear time.

###### Proof.

Let $k$ be the number of 1-clauses (literals) in $F$. If $F$ contains both a
variable and its negation, then $F$ is unsatisfiable, and the number of
satisfying assignments is $0$. Otherwise, the set of literals in $F$ is
consistent, and the number of satisfying assignments is $2^{n-k}$. In either
case, we can compute the desired quantity by scanning through the clauses in
$F$ once. ∎

As two final pieces of notation, we write $A=\text{poly}(B)$ to denote that
$A\leq B^{c}$ for some constant $c>0$, and $A=\exp(B)$ to denote that $A\leq
2^{cB}$ for some constant $c>0$.

###  2.1 Comparison With Related Work

Several works [LV96, Hir98, Tre04, GMR13, LZ19, LSZ19] have considered the
task of approximately counting satisfying assignments to CNF formulas. In
particular, given a constant ${\varepsilon}\in(0,1)$ and CNF formula
$\varphi$, we seek to output an estimate that is within ${\varepsilon}$ of the
true fraction of assignments of $\varphi$ which are satisfying.888One can also
consider _multiplicative_ approximations to $\\#$SAT, but this task is
$\mathsf{NP}$-hard. See for example [Sto85, DL18]. In general, the estimates
provided by such algorithms may be strictly more or less than the true
fraction of satisfying assignments, so such approximation algorithms cannot be
used to solve problems like MAJORITY-$k$SAT.

However, the starting point of our work, the MAJORITY-$2$SAT and
MAJORITY-$3$SAT algorithms, uses methods very similar to those of Trevisan
[Tre04], who showed that for any fixed integer $k$ one can _approximately_
count the fraction of satisfying assignments in a $k$-CNF formula efficiently,
by working with maximal disjoint sets of clauses.999In fact, the second author
devised an algorithm for MAJORITY-$2$SAT in 2004, inspired by Trevisan’s work,
but only recently (with the help of the first author) found a way to
generalize to MAJORITY-$3$SAT and beyond. Given a desired additive
approximation error ${\varepsilon}$, Trevisan’s approach shows that every
$k$-CNF can be _approximated_ by a special kind of decision tree of
$f({\varepsilon},k)\leq O(1)$ size and depth, where the internal nodes are
labeled by variables and the leaves are labeled with 1-CNFs. Computing the
exact fraction of satisfying assignments for such a decision tree is simple to
do in linear time, and Trevisan uses this count to obtain an
${\varepsilon}$-additive approximation of the true fraction of satisfying
assignments.

In our algorithms, we also implicitly (and for MAJORITY-$2$SAT, E-MAJ-$2$SAT,
and MAJ-MAJ-$2$SAT, explicitly) construct such decision tree representations,
and we also use the fact that one can count satisfying assignments exactly on
such decision tree representations. However, for MAJORITY-$k$SAT where $k\geq
3$, our algorithms and analysis have to dig further into the problem and take
advantage of the structure of the decision tree itself. Informally, we show
there are “gaps” in the possible $\\#$SAT values of such representations. Very
roughly speaking, these gaps are part of what allows us to solve the exact
threshold counting problem for $k$-CNFs in polynomial time, “as if” it were an
additive approximation problem. Still, many other cases arise in determining
the fraction exactly that are irrelevant in approximations.

More generally, our algorithms rely on extracting sunflowers from various
subformulas. Sunflower lemmas have been used previously for obtaining additive
approximations to the fraction of satisfying assignments of disjunctive normal
form (DNF) formulas and related problems such as DNF sparsification and
compression [LV96, GMR13, LZ19, LSZ19]. These results typically focused on
formulas of super-constant width, whereas our work is specialized to CNFs of
constant width. Due to our hardness results, one _cannot_ extend our
algorithms to 3CNFs with even one unbounded width clause, unless
$\mathsf{P}=\mathsf{NP}$.

##  3 Threshold SAT for 2-CNFs in Linear Time

As a warm-up, we begin with a simple linear-time algorithm for MAJORITY-$2$SAT
(even THRρ-$2$SAT, for every $\rho\geq 1/\text{poly}(n)$) that illustrates a
few of the ideas.101010The second author has known of this result since around
2004; see Section 7 of [Wil04].

######  Theorem 3.1.

For every rational $\alpha\in(0,1)$, there is an
$m\cdot\text{poly}(1/\alpha)$-time algorithm that, given any 2-CNF formula $F$
on $n$ variables and $m$ clauses, decides whether
$\\#\text{SAT}(F)\geq\alpha\cdot 2^{n}$ or not. Furthermore, when
$\\#\text{SAT}(F)\geq\alpha\cdot 2^{n}$ is true, the algorithm outputs
$\\#\text{SAT}(F)$, along with a a decision tree representation for $F$ of
$\text{poly}(1/\alpha)$ size. The internal nodes are labeled by variables and
leaves are labeled by $1$-CNFs.

###### Proof.

For each $\alpha\in(0,1)$, define
$c(\alpha):=1+\lceil\log_{4/3}(1/\alpha)\rceil$. Note that $c(\alpha)\leq
O(\log\frac{1}{\alpha})$.

Given a 2-CNF $F$, start by finding a _maximal disjoint set_ of clauses $S$.
That is, treat the clauses as sets (ignoring literal signs) and find a set $S$
of clauses such that (a) every pair of clauses in $S$ share no variables and
(b) all other clauses in $F$ contain at least one variable occurring in $S$.
This can be done by greedily choosing the set $S$ (picking disjoint clauses
until we cannot) in time $O(m\cdot|S|)$. We argue that we can stop once $|S|$
exceeds $c(\alpha)$.

Case 1: Suppose $|S|>c(\alpha)$. Then we claim that
$\\#\text{SAT}(F)<\alpha\cdot 2^{n}$. Note that each of the clauses in $S$ are
over disjoint variables, so each clause in $S$ reduces the total number of
satisfying assignments by $3/4$. By our choice of $c(\alpha)$, we have
$(3/4)^{c(\alpha)}<\alpha$. Therefore, less than an $\alpha$-fraction of the
possible assignments satisfy the subformula $S$, and by Proposition 2.4, we
can return NO.

Case 2: Otherwise, $S$ is a maximal disjoint set of clauses with $|S|\leq
c(\alpha)$. Since every clause in $F$ contains at least one variable occurring
in $S$, it follows that, when we plug in any assignment to the variables of
$S$, the remaining formula is a $1$-CNF. Therefore, if we try all of the at
most

$3^{c(\alpha)}\leq O(3^{(\log(\frac{1}{\alpha})/\log(4/3))})\leq
O((1/\alpha)^{\log(3)/\log(4/3)})\leq O((1/\alpha)^{3.82})$

satisfying assignments to the clauses of $S$, and solve $\\#$SAT on the
remaining $1$-CNF formula in $O(m)$ time (Proposition 2.5), we can determine
the number of satisfying assignments _exactly_ in this case.

Note that Case 1 of this algorithm only occurs when
$\\#\text{SAT}(F)<\alpha\cdot 2^{n}$. Consequently, whenever
$\\#\text{SAT}(F)\geq\alpha\cdot 2^{n}$ we fall into Case 2 and our algorithm
reports the exact count of satisfying assignments. The overall run time of
this algorithm is $m\cdot\text{poly}(1/\alpha)$. ∎

It is interesting to contrast the above result with the result of Leslie
Valiant that $\oplus$2SAT is $\oplus$P complete [Val06]. Valiant’s result
implies that computing the low-order bit of $\\#2$SAT in polynomial time would
imply that $\mathsf{NP}\subseteq\mathsf{BPP}$. Our result shows that computing
the low-order bit of $\\#2$SAT looks much more difficult than higher-order
bits.

##  4 Threshold SAT for 3-CNFs in Linear Time

Recall from Definition 2.1 that given a positive integer $k$ and parameter
$\rho\in(0,1)$, we define the “threshold SAT” problem THRρ-$k$SAT to be the
task of deciding whether at least a $\rho$-fraction of assignments to a given
$k$-CNF are satisfying. For example, the MAJORITY-$3$SAT problem discussed
previously is equivalent to THR1/2-3SAT. In this section, we show that for any
$\rho$ with constant numerator and denominator, THRρ-3SAT can be solved in
polynomial time.

More specifically, in Section 4.1 and Section 4.2 we show how to extend the
ideas from Section 3 with a subformula detection argument to prove the
following result.

######  Theorem 4.1.

For every constant $\rho\in[1/2,1]$, we can decide in polynomial time if a
given $3$-CNF on $n$ variables has at least $\rho\cdot 2^{n}$ satisfying
assignments.

In Section 4.3, we generalize these ideas further to solve THRρ-$3$SAT for any
fixed constant threshold $\rho$.

######  Theorem 4.2.

For every positive integer $M$ and for every rational $\rho\in(0,1)$ whose
denominator is bounded above by $M$, THRρ-3SAT can be solved in $O_{M}(n)$
time.

These results will later be subsumed by Theorem 1.1 (showing an analogous
result for all $k\geq 3$), which is proven in Section 5. This section is
included only to present arguments which are less technically challenging, and
therefore hopefully more accessible, while still resolving the complexity of
MAJORITY-$3$SAT. We encourage any reader who becomes bored while reading this
section to jump directly to Section 5. Similarly, the argument in Section 4.3
is self-contained and can be read without referring to Section 4.1 and Section
4.2, even though the motivation for the arguments comes from these earlier
subsections.

###  4.1 Thresholds Greater than One-Half

Building on the MAJORITY-$2$SAT algorithm of Theorem 3.1, we propose the
following natural generalization to 3-CNFs. In the following, a “disjoint set
of clauses” refers to a variable disjoint set (see Definition 2.3).

> Algorithm A. _(With two unspecified constants $c_{1}$ and $c_{2}$.)_
> Given a 3-CNF $F$, find a maximal disjoint set $S$ of clauses of $F$. If
> $|S|$ exceeds a certain constant $c_{1}$, then output NO.
> For all $7^{|S|}$ SAT assignments $A$ to the clauses in $S$, let $F_{A}$ be
> the $2$-CNF induced by assignment $A$, and search for a maximal disjoint set
> $S_{A}$ of 2-clauses in $F_{A}$. If $|S_{A}|$ exceeds a certain constant
> $c_{2}$, then output NO. Otherwise, try all SAT assignments $A^{\prime}$ to
> the clauses in $S_{A}$. For each $1$-CNF formula induced by an $A^{\prime}$,
> count solutions to the $1$-CNF in polynomial time.
> Return YES if and only if the total number of solutions counted (over all
> assignments $A$) is at least $\rho\cdot 2^{n}$.

First, we prove that Algorithm A correctly decides
$\\#\text{SAT}(F)\geq\rho\cdot 2^{n}$ for all fractions $\rho>1/2$.

######  Theorem 4.3.

For every ${\varepsilon}\in(0,1/2]$, we can decide in
$\text{poly}(1/{\varepsilon},n)$ time if a given $3$-CNF on $n$ variables has
at least $(1/2+{\varepsilon})\cdot 2^{n}$ satisfying assignments. Moreover,
given any $3$-CNF with at least $(1/2+{\varepsilon})\cdot 2^{n}$ satisfying
assignments, we can report the exact number of satisfying assignments.

The ability to report the exact number of satisfying assignments will
(provably) no longer hold when we consider the case of ${\varepsilon}=0$, in
the next subsection. This is the major reason why we have treated the two
cases separately.

To prove Theorem 4.3, we show that by setting $c_{1},c_{2}$ appropriately in
Algorithm A, we can decide if there are at least $\rho\cdot 2^{n}$ SAT
assignments for $\rho>1/2$. We first prove a lemma regarding the sizes of
maximal disjoint sets in formulas obtained by assigning variables.

######  Lemma 4.4.

Let $\rho>1/2$, and let $S$ be a maximal disjoint set of $k$-clauses in a
$k$-CNF $F$. Suppose $F$ has at least $\rho\cdot 2^{n}$ satisfying
assignments. For all possible assignments $A$ to the variables of $S$, and for
every induced $2$-CNF $F_{A}$ obtained by assigning $A$ to $S$, $F_{A}$ must
contain a maximal disjoint set of $(k-1)$-clauses of size less than
$2^{k}|S|\ln(1/(\rho-1/2))$.

###### Proof.

The proof is by contrapositive. Let ${\varepsilon}>0$ be such that
$\rho:=1/2+{\varepsilon}$, and let $S$ be a maximal disjoint set of
$k$-clauses in a given $k$-CNF $F$. Suppose there is an assignment $A$ to the
variables of $S$ such that $F_{A}$ has a maximal disjoint set of
$(k-1)$-clauses of size at least $K:=2^{k}|S|\ln(1/{\varepsilon})$. By the
pigeonhole principle, there exists some literal $\ell\in\\{x,\neg x\\}$,
coming from a variable $x$ in the maximal disjoint set $S$, and a set
$T_{\ell}$ of at least $K/(2|S|)=2^{k-1}\ln(1/{\varepsilon})$ clauses in $F$
of the form

$(\ell\vee a_{i,1}\vee\cdots\vee a_{i,k-1})$

where the variables of $a_{i,j}$ are all _distinct_ over all
$i=1,\ldots,|T_{\ell}|$ and $j=1,\ldots,k-1$. That is, the subformula
$T_{\ell}$ of $F$ has in total $1+(k-1)r$ distinct variables, where
$r:=|T_{\ell}|$.

Since $r\geq 2^{k-1}\ln(1/{\varepsilon})$, the fraction of satisfying
assignments in $T_{\ell}$ is at most

$\frac{2^{(k-1)r}+(1-1/2^{k-1})^{r}\cdot
2^{(k-1)r}}{2^{1+(k-1)r}}=\frac{1}{2}+\frac{1}{2}\cdot(1-1/2^{k-1})^{r}\leq\frac{1}{2}+\frac{{\varepsilon}}{2}<\rho,$

where the $2^{(k-1)r}$ term comes from the case where $\ell$ is true, and
$(1-1/2^{k-1})^{r}\cdot 2^{(k-1)r}$ term comes from the case where $\ell$ is
false. Therefore, in such a case, $F$ must have less than a $\rho$ fraction of
satisfying assignments by Proposition 2.4. ∎

We can apply Lemma 4.4 by arguing that, if any subformula $F_{A}$ of $F$ has a
“large” maximal disjoint set of 2-clauses, then we can output NO when
$\rho>1/2$. Otherwise, every $F_{A}$ has a “small” maximal disjoint set of
2-clauses, and Algorithm A works in that case.

Proof of Theorem 4.3.  Let ${\varepsilon}>0$. We consider Algorithm A with
constants $c_{1}:=10$ and $c_{2}:=72\ln(1/{\varepsilon})$.

If $|S|>10$, then the fraction of satisfying assignments to the subformula $S$
is less than $1/2$, therefore $F$ has less than a $1/2$ fraction by
Proposition 2.4. Therefore in step 2 of Algorithm A, we can report NO.

Otherwise, $|S|\leq 9$. Suppose we try all possible satisfying assignments to
$S$ (there are at most $3^{|S|}$) and suppose there is some induced formula
$F_{A}$ with a maximal disjoint set $S_{A}$ of at least
$72\cdot\ln(1/{\varepsilon})$ clauses. By Lemma 4.4 we can deduce that $F$ has
less than an $\rho:=1/2+{\varepsilon}$ fraction of satisfying assignments, and
can report NO.

In the remaining case, every induced formula $F_{A}$ has a maximal disjoint
set $S_{A}$ of less than $72\cdot\ln(1/{\varepsilon})$ clauses. By trying all
possible SAT assignments to each $S_{A}$ (there are
$3^{|S_{A}|}\leq\text{poly}(1/{\varepsilon})$ such assignments) we can count
the number of satisfying assignments for each of the remaining $1$-CNF
formulas in linear time, and determine the exact number of satisfying
assignments by taking the sum of all such counts. $\Box$

###  4.2 Threshold of One-Half

We now we turn to the case of solving THRρ-$3$SAT for threshold value
$\rho=1/2$.

When $\rho=1/2$, Algorithm A does not work correctly in all cases (regardless
of how its parameters are set). Consider a 3-CNF formula $F$ in which every
clause contains a common variable $x$ occurring positively. This is trivially
a YES-instance for MAJORITY-$3$SAT. (Note we cannot efficiently compute the
number of satisfying assignments exactly in this case, as it would solve the
$\\#2$SAT problem in polynomial time!) Running Algorithm A on $F$, it will
find an $S$ with $|S|=1$, since $x$ appears in all clauses. When we try all
satisfying assignments to $S$, and $x$ is set true, the formula becomes a
tautology. But when $x$ is set false, the formula becomes an arbitrary
$2$-CNF, with potentially a very large disjoint clause set. Regardless of the
size of that clause set, the original $F$ is still a YES instance, even if
_all_ of the clauses in the remaining $2$-CNF are disjoint. So, an algorithm
for MAJORITY-3SAT needs to be able to account for this sort of behavior, where
a single literal appears in many clauses.

To handle this case, we introduce a check for another type of “bad”
subformula.

######  Lemma 4.5.

Let $\ell\in\\{x,\neg x\\}$ be a literal, and let

$S=\\{(\ell\vee a_{1}\vee b_{1}),\ldots,(\ell\vee a_{t}\vee b_{t}),(u\vee
v\vee w)\\}$

be a set of clauses with the following properties:

  * •

For all $i,j\in[t]$, $a_{i}$ and $b_{j}$ are literals from $2t$ distinct
variables, all of which are different from $x$.

  * •

The literal $\ell$ does not appear in $(u\vee v\vee w)$ (however, $\neg\ell$
may appear in $(u\vee v\vee w)$).

Then for all $t\geq 8$, $S$ has less than $2^{r-1}$ satisfying assignments,
where $r$ is the total number of variables occurring in $S$.

###### Proof.

Let $r$ be the total number of variables in $S$; note that $r\geq 2t+1$. When
$\ell$ is set to false, the $t$ clauses $(a_{i}\vee b_{i})$ are all disjoint,
so the formula $S$ has at most $(3/4)^{t}\cdot 2^{r-1}$ satisfying assignments
over the remaining $r-1$ variables. When $\ell$ is true, the clause $(u\vee
v\vee w)$ remains, so (over the remaining $r-1$ variables) the number of
satisfying assignments in this case is at most $(7/8)\cdot 2^{r-1}$ (note that
if the literal $\neg\ell$ appears in $(u\vee v\vee w)$, then the fraction is
$3/4$, which is only better for us). For $t\geq 8$, the total number of
satisfying assignments is therefore $((3/4)^{t}+7/8)\cdot 2^{r-1}<2^{r-1}$. ∎

For $t$ sufficiently large, Lemma 4.5 can be used to show that $S$ has less
than $(7/16+{\varepsilon})2^{r}$ satisfying assignments for any desired
${\varepsilon}>0$.

#### MAJ3SAT in $\mathsf{P}$.

We are now ready to give a polynomial-time algorithm for deciding if a $3$-CNF
has at least $2^{n-1}$ satisfying assignments. For ease of reading, here we
will describe the algorithm alongside its analysis.

Given a $3$-CNF $F$ on $n$ variables, we start by checking if there is a
common literal $\ell$ appearing in every clause of $F$. In this case we output
YES, as any such formula is satisfied by at least half of its assignments.

After this point, we know:

> $(\star)$ For every literal $\ell$ there is at least one clause in $F$ that
> does not contain $\ell$.

Next, we find a maximal disjoint set $S$ among the 3-clauses in $F$. If
$|S|\geq 6$ then, since $(7/8)^{6}<0.449<1/2$, we can output NO by Proposition
2.4.

Otherwise, we know that $|S|\leq 5$. For each of the $7^{|S|}$ satisfying
assignments $A$ to the clauses of $S$, we do the following:

For each $2$-CNF formula $F_{A}$ induced by an assignment $A$ on the variables
of $S$ in $F$, find a maximal disjoint set $S_{A}$ over the 2-clauses in
$F_{A}$.

  1. 1.

We claim that, if there is an assignment $A$ such that $|S_{A}|\geq 48|S|+2$,
then $F$ must contain less than $2^{n-1}$ satisfying assignments. Hence we can
output NO in this case.

This paragraph proves the claim. For each 2-clause $(x\vee y)$ in $S_{A}$,
select one clause from $F$ that $(x\vee y)$ arose from: such a clause is
either of the form $(\ell\vee x\vee y)$ where $\ell$ is a literal whose
variable appears in $S$, or it is simply $(x\vee y)$ ($F$ may contain
2-clauses itself). Put each such clause from $F$ into a new set
$S^{\prime}_{A}$, so that $|S^{\prime}_{A}|=|S_{A}|$. Suppose there are at
least three 2-clauses in $S^{\prime}_{A}$. Since these 2-clauses are disjoint
and appear in $F$, the subformula of $S^{\prime}_{A}$ restricted to these
2-clauses is a subformula of $F$ and must have at most a $(3/4)^{3}<0.422<1/2$
fraction of satisfying assignments. By Proposition 2.4, $F$ has less than
$0.422\cdot 2^{n}$ satisfying assignments in this case. Otherwise, there are
at most two $2$-clauses in $S^{\prime}_{A}$. Removing them from
$S^{\prime}_{A}$, there are still at least $48|S|$ 3-clauses. As there are
$3|S|$ distinct variables appearing in $S$, and hence $6|S|$ literals whose
variable appears in $S$, there must be a literal $\ell$ whose variable appears
in $S$ such that $\ell$ appears in at least $8$ clauses of $S^{\prime}_{A}$.
By property $(\star)$ above, it follows that there is a subformula in $F$
satisfying Lemma 4.5. Therefore $F$ has less than $\rho 2^{n}$ satisfying
assignments for a constant $\rho<1/2$.

  2. 2.

Otherwise, for all assignments $A$, we have $|S_{A}|<48|S|$. In this case, we
can try all $3^{|S_{A}|}$ satisfying assignments $A^{\prime}$ to the 2-clauses
in $S_{A}$. Since $S_{A}$ is a maximal disjoint set of 2-clauses in $F_{A}$,
every formula obtained by plugging in $A^{\prime}$ is a $1$-CNF formula. We
solve $\\#$SAT on the resulting $1$-CNF formula in linear time, and add the
number to a running sum (calculated over all choices $A$ and $A^{\prime}$).

Finally, output YES if the total sum of satisfying assignments exceeds
$2^{n-1}$, otherwise output NO. This completes the description of the
algorithm, and its analysis.

It is interesting to observe that, no matter what $3$-CNF formula is provided,
at least one of the following conditions is true at the end of the algorithm:

  * (a)

There are at least $2^{n-1}$ satisfying assignments (an early YES case).

  * (b)

There are at most $\rho 2^{n}$ satisfying assignments, for a constant
$\rho<1/2$ (an early NO case).

  * (c)

The number of satisfying assignments is counted exactly.

Therefore, for any $3$-CNF formula in which the $\\#$SAT value is strictly
between $\rho 2^{n}$ and $2^{n-1}$, the above algorithm actually computes the
$\\#$SAT value exactly.

Note that the above algorithm runs in linear time, although the constant
factor in the worst case (enumeration over partial assignments) is at least
$7^{5}\cdot 3^{48\cdot 5-1}>10^{118}$. Of course, in order to give a succinct
proof, we have been extremely loose with the analysis; a smaller constant
factor is certainly possible.

###  4.3 Generalizing to All Thresholds

In this subsection we finish the proof of Theorem 4.2, handling the case of
fractions $\rho<1/2$.

#### Some Lemmas.

The below lemma will be used to show that there must be certain “gaps” in the
numbers of satisfying assignments to a $k$-CNF formula. This will aid in the
detection of YES and NO instances of Threshold SAT.

######  Lemma 4.6.

Let $n$ and $m$ be arbitrary positive integers, and let $\rho\in(0,1)$ be
rational, of the form

$\rho=\frac{a}{2^{v}b}$

for unique odd integer $b$, nonnegative integer $v$, and integer $a$ with
$\gcd(a,2^{v}b)=1$. Then for every integer $N$ which is the sum of at most $m$
powers of two, if $N<\rho 2^{n}$ then $N\leq\left(\rho-\eta\right)2^{n}$, for
a positive $\eta$ depending only on $a,b,v$, and $m$.

The proof of the above result follows from casework on the binary expansion of
$\rho$, and is presented in Appendix B. Lemma 4.6 formalizes the intuition
that if we want to maximize the sum of $m$ powers of two with the constraint
that the sum is strictly less than $\rho=a/b$, the best one can do is to
greedily pick distinct powers of $2$ (i.e. binary digits) whose total sum is
never at least $\rho$. The proof in Appendix B shows that when $b$ is a power
of $2$, we can take

$\eta\geq\frac{\rho}{2^{m+c}}$

for some constant $c$. For general $\rho$ the decay in terms of $m$ could be
much worse, but can still bounded below as

$\eta\geq\frac{\rho}{2^{(b-1)m+c}}.$

We will also need the following structural lemma, that lets us extract simple
certificates that a $3$-CNF has a small fraction of satisfying assignments. To
state this lemma, recall we defined a _variable-disjoint set_ $D$ (Definition
2.3) to be a collection of clauses such that no two distinct clauses in $D$
have literals corresponding to the same variable. In other words, if we view
the clauses of $D$ as sets of variables, the sets are pairwise disjoint. The
following is a natural generalization of this definition.

######  Definition 4.7 (Sunflowers).

Let $w$ be a nonnegative integer. A set $S$ of clauses is called a _$w$
-sunflower_ if there exists a set $L$ of $w$ distinct literals, such that
every clause in $S$ contains the literals of $L$, and removing the literals of
$L$ from each clause of $S$ produces a variable-disjoint set. A set of clauses
is a _sunflower_ if it is a $w$-sunflower for some nonnegative $w$. The _core_
of a sunflower is the set $L$, the sunflower’s _weight_ is the size of its
core $w$, and the sunflower has _size_ $|S|$.

Note that a $0$-sunflower is just a disjoint set. In our algorithms, we will
always work with sunflowers whose cores are consistent sets (Definition 2.2),
which implies there is an assignment to just the core variables which
satisfies all clauses in the sunflower.

Our key lemma describes an algorithm which takes a $3$-CNF $F$ as input, and
either finds a large $0$-sunflower in $F$, a large $1$-sunflower in $F$, or it
decomposes $F$ into a short list of $1$-CNFs. The proof below is just a more
sophisticated restatement of arguments from previous subsections, but it will
be a useful framework for generalizing to the case of $k\geq 4$.

######  Lemma 4.8 (Sunflower Extraction in a 3-CNF).

Let $Z$ and $Q$ be positive integers. There is an algorithm which, given a
$3$-CNF $F$, runs in

$O\left(7^{Z}3^{3ZQ}\cdot|F|\right)$

time, where $|F|$ is the size of the input formula, and either

  * •

outputs a 0-sunflower of size $Z$ in $F$, or

  * •

outputs a 1-sunflower of size $Q$ in $F$, or

  * •

outputs a list of $m\leq 7^{Z}3^{3ZQ}$ 1-CNFs such that the number of
satisfying assignments in $F$ equals the sum of $\\#\text{SAT}(F^{\prime})$
over all 1-CNFs $F^{\prime}$ in the list.

###### Proof.

We will prove the result by repeatedly extracting maximal disjoint sets from
the formula $F$ in a greedy manner. If the sets we find are “large,” we will
output a sunflower; otherwise, we can loop over all satisfying assignments to
some “small” disjoint sets and recover a list of 1-CNFs.

We begin by scanning through the clauses of $F$ to build a maximal variable
disjoint set $S$. If $|S|\geq Z$, return the $0$-sunflower $S$ and halt.

Otherwise, $|S|<Z$. We enumerate all $7^{|S|}<7^{Z}$ satisfying assignments
$\alpha$ to $S$. For each $\alpha$, we produce a new formula $F_{\alpha}$
obtained from $F$ by assigning values to the variables of $S$ according to
$\alpha$. Since $S$ is a _maximal_ disjoint set and we assigned all variables
in $S$, it follows that $F_{\alpha}$ is a $2$-CNF. Next, we process the
$F_{\alpha}$ in the order they are produced. For each $F_{\alpha}$, scan
through its clauses and build a maximal variable disjoint set $S_{\alpha}$ of
width-two clauses. We distinguish between two cases, according to whether this
set is large or small.

Case 1:  $|S_{\alpha}|\geq 3Q|S|$.

In this case, we show how to return a large 1-sunflower.

Since the variables in $S_{\alpha}$ are a “hitting set” for the clauses of
$F$, and since $S_{\alpha}$ has width-two clauses, each clause of $S_{\alpha}$
was formed in $F_{\alpha}$ by removing exactly one literal corresponding to a
variable in $S$, from some clause in $F$.

Since $S$ is a variable disjoint set in a $3$-CNF, the number of variables
appearing in $S$ is at most $3|S|$. Under an assignment $\alpha$ to $S$, we
remove a literal $\ell$ from a clause in $F$ to produce $F_{\alpha}$ if and
only if $\alpha$ assigns $\ell$ to be false. Thus, at most $3|S|$ literals
were removed to produce the clauses in $S_{\alpha}$.

By averaging/pigeonhole, there is some literal $\ell$ and there are at least

$\frac{|S_{\alpha}|}{3|S|}\geq Q$

clauses in $S_{\alpha}$ whose corresponding clauses in $F$ all contain $\ell$.
We can find such a literal $\ell$ and set of clauses simply by scanning
through the clauses in $F$ and $S_{\alpha}$. Because $S_{\alpha}$ was a
variable-disjoint set, the resulting set of clauses forms a $1$-sunflower of
size at least $Q$ in $F$, which we can then return.

Case 2:  $|S_{\alpha}|<3Q|S|$.

In this scenario, we just loop over all $3^{|S_{\alpha}|}<3^{3ZQ}$ satisfying
assignments $\beta$ to $S_{\alpha}$, noting that each 2-clause has precisely
$3$ assignments to the variables it contains which can satisfy it, and no two
clauses share variables. For each produce a new formula $F_{\alpha,\beta}$
induced from $F_{\alpha}$ by assigning values to its variables according to
$\beta$. Every clause of width two in $F_{\alpha}$ has a literal whose value
gets assigned in this process (since we chose $S_{\alpha}$ was chosen to be
maximal) so the resulting formula $F_{\alpha,\beta}$ is a 1-CNF.

Thus the set of satisfying assignments in $F$ can be found just by taking the
union over all partial assignments $\alpha$ and $\beta$, and counting
satisfying assignments for the resulting 1-CNFs $F_{\alpha,\beta}$. So in this
case we just return the list of all 1-CNFs produced in this way. This list has
at most $7^{Z}3^{3ZQ}$ formulas, as desired. ∎

With these two results, we are now ready to prove the main theorem of this
section.

###### Proof of Theorem 4.2.

Let $\varphi$ be the input $3$-CNF on $n$ variables.

Set $z:=\Theta(\log(1/\rho))$ to be the smallest positive integer such that

$(7/8)^{z}<\rho.$

The variable $z$ will be our cutoff value for a 0-sunflower being “large.”

Set $t:=\lfloor\log(1/\rho)\rfloor$ to be the unique nonnegative integer such
that

$(1/2)^{t}\geq\rho>(1/2)^{t+1}.$

Let $q_{0}>\dots>q_{t}>0$ be integer parameters to be specified later. The
$q_{r}$ constants will determine the cutoffs for 1-sunflowers to be considered
“large.” For now, we take $q_{t}$ large enough so that

$(3/4)^{q_{t}}<\frac{\rho-(7/8)^{z}}{t+1}.$ (2)

Since the denominator of $\rho$ is bounded above by some constant $M$, the
above inequality holds provided we take $q_{t}\geq\Omega(z\log M)$.

With this setup, we present the algorithm for THRρ-3SAT below. The steps of
the algorithm which could return an answer are annotated with case numbers,
which correspond to the cases we examine later when arguing correctness. The
routine also sets the value of a parameter $r$, which corresponds to the
number of large 1-sunflowers we end up discovering. The symbol $\rhd$
indicates the beginning of a comment which provides context for a given step,
and is not part of the algorithm description.

  1. 1.

Initialize $F=\varphi$.

  2. 2.

Initialize $r=0$.

  3. 3.

While $r\leq t$:

    1. (i)

Run the algorithm of Lemma 4.8 with $Z=z$ and $Q=q_{r}$.

    2. (ii)

If step 3(i) returns a 0-sunflower of size at least $Z$, then return NO.

(Case 1)

    3. (iii)

If step 3(i) returns a 1-sunflower of size at least $Q$, save this sunflower
$S$ and its core $C=\\{\ell\\}$. Then scan through $F$ to find the set of all
clauses $F^{\prime}$ in $F$ containing the literal $\ell$.

Let $G$ be the set of clauses formed by taking $F\setminus F^{\prime}$ and
removing all instances of the literal $\lnot\ell$. Update the value of the
formula $F\leftarrow G$.

> $\rhd$ The above step just asserts that $\ell$ is true in $F$.

Increment $r\leftarrow r+1$.

If the new $F$ is empty (has no clauses) and $r\leq t$, then return YES.

(Case 2)

> $\rhd$ We check that $r\leq t$ since in the case where $r=t+1$ after being
> incremented, halting at this step means we have a hitting set of $t+1$
> literals on the clauses of $F$, which is not necessarily a YES case.

    4. (iv)

Otherwise, step 3(i) returns a list $L$ of $m\leq\exp(z\cdot q_{r})$ 1-CNFs.

Use this list to compute the fraction of satisfying assignments of $F$. If
this fraction is at least $\rho$ then return YES, otherwise return NO.

(Case 3)

  4. 4.

If the while loop completes without early halting, return NO.

(Case 4)

Recall that running the sunflower extraction procedure from Lemma 4.8 on a
formula $F$ with parameters $Z$ and $Q$ takes $O\left(f(Z,Q)|F|\right)$ time
where $f(Z,Q):=7^{Z}3^{3ZQ}$. Consequently, the above algorithm takes
asymptotically at most

$\left(f(z,q_{0})+f(z,q_{1})+\dots+f(z,q_{t})\right)|\varphi|$ (3)

time.

Suppose that before halting, the algorithm completes $r$ iterations of step
3(iii) in the while loop. At this point, we have discovered literals
$\left\\{\ell_{i}\right\\}_{1\leq i\leq r}$ and a sequence of $3$-CNFs
$\left\\{F_{i}\right\\}_{0\leq i\leq r}$ such that

  1. 1.

$F_{0}=\varphi$,

  2. 2.

$F_{i-1}$ contains a 1-sunflower of size $q_{i-1}$ with core $\\{\ell_{i}\\}$,
and

  3. 3.

$F_{i}$ is induced from $F_{i-1}$ by setting $\ell_{i}$ to be true

for $1\leq i\leq r$.

The following observation helps us argue that only a negligible fraction of
satisfying assignments of $\varphi$ do not set all of the $\ell_{i}$ to be
true.

######  Claim 4.9.

The fraction of assignments which set some $\ell_{i}$ to be false and satisfy
$\varphi$ is less than

$r\cdot(3/4)^{q_{r-1}}.$

Equivalently, we have

$\Pr[\varphi\land\left(\lnot\ell_{1}\lor\lnot\ell_{2}\lor\dots\lor\lnot\ell_{r}\right)]<r\cdot(3/4)^{q_{r-1}}<\rho-(7/8)^{z}.$

###### Proof.

Take any index $1\leq i\leq r$. Then if we set $\ell_{i}$ to be false, and
$\ell_{j}$ to be true for all $j<i$, the resulting formula contains a
0-sunflower of size at least $q_{r-1}\geq q_{t}$ with clauses of width at most
two. This follows from points 2 and 3 above, which define the $F_{j}$
formulas. The fraction of assignments to variables in the resulting formula
that can satisfy it is at most

$(3/4)^{q_{r-1}}\leq(3/4)^{q_{t}}<\frac{\rho-(7/8)^{z}}{t+1}$

by our choice of $q_{t}$. Now, by considering the minimum index $i$ with
$\ell_{i}$ set to false, we see that

$\Pr[\varphi\land\left(\lnot\ell_{1}\lor\lnot\ell_{2}\lor\dots\lor\lnot\ell_{r}\right)]=\Pr[\varphi\land\lnot\ell_{1}]+\Pr[\varphi\land\ell_{1}\land\lnot\ell_{2}]+\dots+\Pr[\varphi\land\ell_{1}\land\ell_{2}\dots\land\lnot\ell_{r}].$

By the above discussion, each term on the right hand side is less than
$(3/4)^{q_{r-1}}$. Thus we have

$\Pr[\varphi\land\left(\lnot\ell_{1}\lor\lnot\ell_{2}\lor\dots\lor\lnot\ell_{r}\right)]<r\cdot(3/4)^{q_{r-1}}<\rho-(7/8)^{z}$

as claimed. ∎

We now perform casework on the four distinct ways the above procedure could
halt, and in each scenario show that the algorithm returns the correct answer
for the THRρ-3SAT problem.

Case 1: Large 0-Sunflower

Suppose we halt in step 3(i). Then we found a 0-sunflower $S$ of size at least
$z$ in $F_{r}$.

Consequently, if the literals $\left\\{\ell_{i}\right\\}_{1\leq i\leq r}$ are
all set true, to satisfy $\varphi$ we still need to satisfy $S$, which is
satisfied by at most a

$(7/8)^{z}<\rho$

fraction of assignments to its own variables (which are disjoint from the
$\ell_{i}$). In other words, we have

$\Pr[\varphi\land\left(\ell_{1}\land\ell_{2}\land\dots\land\ell_{r}\right)]<(7/8)^{z}.$

Combining this observation with 4.9, which shows that the fraction of
assignments which satisfy $\varphi$ and set some $\ell_{i}$ to be false is
less than $\rho-(7/8)^{z}$, we deduce that $\Pr[\varphi]<\rho$, so reporting
NO is correct.

Case 2: Small Covering by Cores

Suppose we halt in step 3(iii) because the formula $F$ became empty when
$r\leq t$.

Then this means that there exists a consistent set of at most $t$ literals
$\ell_{1},\dots,\ell_{r}$ (corresponding to the cores of 1-sunflowers found in
the procedure) corresponding to distinct variables such that every clause in
the original formula contains at least one of these literals.

Consequently, any assignment that sets these literals to true is a satisfying
assignment. It follows that at least a

$1/2^{t}\geq\rho$

fraction of assignments to $\varphi$ are satisfying, so returning YES is
correct.

Case 3: Exact Count on Subformula

Suppose we halt in step 3(iv) because we obtained a list of 1-CNFs for
$F_{r}$.

This list contains at most $m\leq f(z,q_{r})$ formulas. Using Proposition 2.5,
in $O(m|\varphi|)$ time we can count the number of satisfying assignments for
each formula in this list. Let the sum of these counts be $N$. By Proposition
2.5 we know that $N$ is the sum of at most $m$ powers of two, and by Lemma 4.8
we have

$\\#\text{SAT}(F_{r})=N$

where $F_{r}$ is viewed as a formula on $n-r$ variables (the original
variables of $\varphi$, with the variables corresponding to
$\ell_{1},\dots,\ell_{r}$ removed).

If $N\geq\rho 2^{n}$ then we can immediately report YES, because the
satisfying assignments where we set all the $\ell_{i}$ to be true already
account for at least a $\rho$-fraction of all assignments.

Otherwise, $N<\rho 2^{n}$. Then by Lemma 4.6, there exists an $\eta>0$
depending on $\rho$ and $m$ such that

$N\leq(\rho-\eta)2^{n}.$

In other words, the fraction of assignments which set all of the $\ell_{i}$ to
true and satisfy $\varphi$ is at most

$\frac{N}{2^{n}}\leq\rho-\eta.$

By 4.9, the fraction of assignments which set some $\ell_{i}$ to false and
satisfy $\varphi$ is less than

$r\cdot\left(3/4\right)^{q_{r-1}}.$

It follows that the fraction of satisfying assignments of $\varphi$ is at most

$\Pr[\varphi]<r\cdot\left(3/4\right)^{q_{r-1}}+(\rho-\eta)=\rho+\left[r\cdot\left(3/4\right)^{q_{r-1}}-\eta\right].$

Thus, if we pick each $q_{r-1}$ large enough that

$r\cdot\left(\frac{3}{4}\right)^{q_{r-1}}<\eta$

we necessarily have $\\#\text{SAT}(\varphi)<\rho 2^{n}$ and can report NO.

Case 4: Many Large 1-Sunflowers

Suppose the routine halts because we set $r=t+1$ (terminating the loop).

Then the fraction of assignments which satisfy $\varphi$ and set all the
$\ell_{i}$ to true is at most

$(1/2)^{t+1}$

since the literals $\ell_{i}$ come from different variables.

By 4.9, the fraction of assignments which satisfy $\varphi$ and set some
$\ell_{i}$ to false is at most

$(t+1)\cdot(3/4)^{q_{t}}.$

Consequently, the fraction of satisfying assignments in $\varphi$ is at most

$\Pr[\varphi]<\frac{1}{2^{t+1}}+(t+1)\cdot\left(\frac{3}{4}\right)^{q_{t}}.$

So if we take $q_{t}$ large enough that

$(t+1)\cdot\left(\frac{3}{4}\right)^{q_{t}}<\rho-(1/2)^{t+1}$

then the total fraction of satisfying assignments of $\varphi$ is strictly
less than $\rho$ so we can report NO in this case as well. Note that our
choice of $t$ ensures that the right hand side is positive. Moreover, if
$\rho$ has denominator bounded above by a constant $b$, the right hand side is
bounded below by $1/(b2^{t+1})$ so there is some constant $q_{t}$ satisfying
the above inequality.

This handles all possible ways the routine could terminate. The arguments
above show that provided we set $q_{t}$ large enough in terms of $\rho$ and
$M$, and then recursively set $q_{r-1}$ large enough in terms of $q_{r}$ for
each possible value $t\leq r\leq 1$, the algorithm is correct (the precise
choice of parameter values is described in more detail in Appendix C). If the
upper bound $M$ on the denominator of $\rho$ is a constant, then the factor
multiplied to $|\varphi|$ in the time bound of eq. 3 is also a constant
depending on $M$, so the algorithm runs in linear time as desired. ∎

Getting a precise bound on the runtime of Theorem 4.2 is difficult, as it
depends on $\rho$ in subtle ways. However, we can give a very loose upper
bound on the worst case runtime of the algorithm’s dependence on $\rho$.
Recall that $A=\text{poly}(B)$ means that $A\leq B^{O(1)}$.

######  Proposition 4.10.

Let $\rho\in(0,1)$ be a rational with denominator $b$. Set
$t=\lfloor\log(1/\rho)\rfloor$. Then there exists $K=\text{poly}(1/\rho)$ such
that if we define

$c=\underbrace{K^{\cdot^{\cdot^{K^{(\log b)}}}}}_{t+2\text{ terms}}$

to be a tower of $t+1$ exponentiations of $K$ together with one exponentiation
to the $(\log b)^{\text{th}}$ power at the top of the tower, the THRρ-3SAT
algorithm described in the proof of Theorem 1.1 takes at most

$c|\varphi|$

time.

We prove the above result in Appendix C.

######  Remark 4.11 (Similarity to Regularity Lemmas).

Although the runtime described in Proposition 4.10 increases horrendously
quickly as $\rho$ gets smaller, this tower-of-exponents dependence on $1/\rho$
is perhaps not too surprising, given the similarities between our approach and
other “regularity lemma” approaches. Roughly speaking, a regularity lemma is a
structural theorem for some class of combinatorial objects, which states that
given some fixed robustness parameter ${\varepsilon}$, any object from the
class has a “small-sized” (depending on ${\varepsilon}$) structured
representation, provided we are allowed to make some “small” (again depending
on ${\varepsilon}$) number of modifications to the object.

Examples include Szemerédi’s classic graph regularity lemma [Sze75] and a
recent set regularity lemma used for graph coloring algorithms [Zam20]. In
both these examples, the size of the structured representation grows like a
tower of exponentials whose height is polynomial in $1/{\varepsilon}$, and
there are proofs showing that any approach using these regularity lemmas
requires such a rapid growth [Gow97, MS14, Zam20].

Our algorithm can be viewed from this same perspective: given a 3-CNF and
fixed threshold $\rho$ we find a constant number of literals whose values we
can set, after which point the modified formula has a solution space which can
be decomposed into a disjoint union of solutions to 1-CNFs (the structured
representation). It turns out that a similar statement holds more generally
for $k$-CNFs.

##  5 Threshold SAT on General Bounded Width CNFs

In this section, we show how to extend the results of the previous section to
detect whether the fraction of satisfying assignments in a given $k$-CNF is at
least $\rho=a/b$ in polynomial time, when the clause width $k$ and denominator
of the threshold $b$ are fixed positive integers.

Reminder of Theorem 1.1.  For every constant rational $\rho\in(0,1)$ and
constant integer $k$, there is a deterministic linear-time algorithm that
given a $k$-CNF $F$ determines whether or not $\\#\text{SAT}(F)\geq\rho\cdot
2^{n}$.

The proof extends the ideas employed in the proof of Theorem 4.2 even further.
We will need the following generalization of Lemma 4.8, to extract sunflowers
in CNFs of width greater than three.

######  Lemma 5.1 (Sunflower Extraction Algorithm).

Fix positive integers $Q_{0},Q_{1},\dots,Q_{k-2}$. There is a computable
function $f$ and an algorithm which runs in at most

$f(Q_{0},Q_{1},\dots,Q_{k-2})\cdot|F|$

time on any given $k$-CNF $F$, which either

  * •

produces a $v$-sunflower of size at least $Q_{w}$ in $F$ for some
$w\in\left\\{0,1,\dots,k-2\right\\}$ and $v<w$, or

  * •

produces a collection ${\cal C}$ of $1$-CNF formulas such that $|{\cal C}|\leq
f(Q_{0},Q_{1},\dots,Q_{k-2})$ and

$\\#\text{SAT}(F)=\sum_{F^{\prime}\in{\cal C}}\\#\text{SAT}(F^{\prime}).$

That is, $\\#\text{SAT}(F)$ equals the sum of $\\#\text{SAT}(F^{\prime})$ over
all $1$-CNFs $F^{\prime}$ in ${\cal C}$.

We prove Lemma 5.1 in Appendix A, using an inductive argument very similar to
the proof of the classic sunflower lemma [ER60] and the proof of Lemma 4.8.

######  Theorem 5.2.

For every positive integer $k$ and for every rational $\rho\in(0,1)$ whose
denominator is bounded above by some constant $M$, THRρ-$k$SAT can be solved
deterministically on input $\varphi$ in $O_{M,k}(|\varphi|)$ time.

###### Proof.

The intuition behind the proof is provided in Section 1.2. Here we briefly
recall the idea before proceeding formally. For a $k$-CNF $\varphi$, we want
to decide whether

$\Pr[\varphi]\geq\rho.$

We will do this by constructing a special $(k-2)$-CNF $\psi$ over the same
variable set, splitting the probability calculation into

$\Pr[\varphi]=\Pr[\varphi\land\psi]+\Pr[\varphi\land\lnot\psi].$

Observe that

$\Pr[\varphi\land\psi]\leq\Pr[\varphi]=\Pr[\varphi\land\psi]+\Pr[\varphi\land\lnot\psi].$
(4)

Intuitively, we construct $\psi$ in such a way that
$\Pr[\varphi\land\lnot\psi]<{\varepsilon}_{1}$ for an _extremely_ small
${\varepsilon}_{1}>0$, so that it is possible to reduce the problem
THRρ-$k$SAT on $\varphi$ to THRρ-$k$SAT on $\varphi\land\psi$. We pick $\psi$
so that $\varphi\land\psi$ can be significantly simplified, making the new
formula easier to work with.

On a first read, it may be easier to ignore the precise bounds we require for
each constant, and instead just check which variables correspond to the values
of sunflower sizes and sunflower counts.

#### Beginning of parameters.

Let $z$ be the smallest positive integer such that
$\left(1-\frac{1}{2^{k}}\right)^{z}<\rho$.

As in the proof of Theorem 4.2, the parameter $z$ is our cutoff value for a
large 0-sunflower.

For convenience we write

$\alpha:=\rho-\left(1-\frac{1}{2^{k}}\right)^{z}$ (5)

which will be a useful upper bound on fractions of satisfying assignments.
Note that because $\rho$ has denominator bounded above by some constant $M$,
$\alpha$ is bounded below by some function of $M$ and $k$.

Let $t_{1}:=\lceil\log 1/\rho\rceil$ be the smallest positive integer such
that $(1/2)^{t_{1}-1}>\rho\geq(1/2)^{t_{1}}.$ This is analogous to the
parameter $t$ introduced in the proof of Theorem 4.2.

The constant $t_{1}$ represents the maximum number of 1-sunflowers we will
search for.

We then take parameters

$q_{1}(0)>q_{1}(1)>\dots>q_{1}(t_{1}-1)$

where $q_{1}(r_{1})$ denotes the size of the $1$-sunflower we look for,
assuming we have already found $r_{1}$ sunflowers of weight $1$ (recall that
we defined the _weight_ of a sunflower to be the size of its core). We will
describe the values of these parameters later in the proof.

We introduce similar parameters for sunflowers of larger weight, but the setup
is more involved. For each possible index $0\leq r_{1}\leq t_{1}-1$ we
introduce a parameter $t_{2}(r_{1})$ to be determined, and then additionally
take a sequence of constants

$q_{2}(r_{1},0)>q_{2}(r_{1},1)>\dots>q_{2}(r_{1},t_{2}(r_{1})-1).$

More generally, for each $2\leq w\leq k-2$, assuming we have defined some
$t_{v}$ and $q_{v}$ sequences for $v<w$, for each choice of arguments $0\leq
r_{v}\leq t_{v}(r_{1},\dots,r_{v-1})-1$, we recursively define a parameter

$t_{w}(r_{1},r_{2},\dots,r_{w-1})$

together with a sequence of constants

$q_{w}(r_{1},r_{2},\dots,0)>q_{w}(r_{1},r_{2},\dots,1)>\dots>q_{w}(r_{1},r_{2},\dots,t-1)$

where $t=t_{w}(r_{1},r_{2},\dots,r_{w-1})$.

Intuitively, $t_{w}(r_{1},\dots,r_{w-1})$ denotes the maximum number of
_additional $w$-sunflowers we will search for_, and the constant
$q_{w}(r_{1},\dots,r_{w-1},r_{w})$ represents the size of the $w$-sunflower we
are looking for, assuming that thus far we have found precisely $r_{v}$ large
$v$-sunflowers for each $v<w$.

For every $1\leq w\leq k-2$, we also define the constant

$T_{w}=\prod_{v=1}^{w-1}\max_{r_{1},\dots,r_{v-1}}t_{v}(r_{1},\dots,r_{v-1}).$

The maximums taken in each factor on the right hand side above are taken over
sequences $(r_{1},\dots,r_{v-1})$ which which satisfy $0\leq r_{u}\leq
t_{u}(r_{1},\dots,r_{u-1})-1$ for all $u\leq v-1$. The constant $T_{w}$ is
just an upper bound on how many different values of $(r_{1},\dots,r_{w-1})$ we
will ever consider (because there are at most $t_{1}$ choices of $r_{1}$, then
at most $\max_{r_{1}}t_{2}(r_{1})$ choices of $r_{2}$, etc.).

For convenience, we typically abbreviate $\vec{r}=(r_{1},r_{2},\dots,r_{k-2})$
and $\vec{r}[v]=(r_{1},\dots,r_{v})$. This allows us to write
$t_{w}(\vec{r}[w-1])$ and $q_{w}(\vec{r}[w])$ instead of
$t_{w}(r_{1},\dots,r_{w-1})$ and $q_{w}(r_{2},\dots,r_{w})$, where it is
understood that the entries of $\vec{r}$ satisfy the appropriate inequalities
of $0\leq r_{v}\leq t_{v}(\vec{r}[v-1])-1$ for each $v\leq w$.

We will describe the values of all these constants near the end of the proof.
For now, we note some bounds they must satisfy. Define

$\beta=\rho-\frac{1}{2^{t_{1}}}\left(1-\frac{1}{2^{k}}\right).$ (6)

The above quantity is positive by our choice of $t_{1}$. Like $\alpha$, the
quantity $\beta$ is another useful upper bound on the fraction of satisfying
assignments a formula has, and is bounded below by some function of $M$ and
$k$.

We then set the $q_{w}$ parameters large enough that

$\left(1-\frac{1}{2^{k-w}}\right)^{q_{w}(\vec{r}[w])}<\frac{\min(\alpha,\beta)}{(k-2)T_{w}\cdot
t_{w}(\vec{r}[w-1])}.$ (7)

for all $\vec{r}$ and $w\geq 2$. We can ensure this holds by making sure
$q_{w}(\vec{r}[w])$ is large enough in terms of $T_{w}$ and
$t_{w}(\vec{r}[w-1])$ for all $\vec{r}$. In other words, we just need to pick
each $q_{w}(\vec{r}[w])$ large enough in terms of $t_{w}(\vec{r}[w-1])$ and
$t_{v}(\vec{s}[v-1])$ for all $\vec{s}$ and $v<w$.
End of parameters.

#### How the Algorithm Works.

At a high level, the algorithm proceeds by scanning through $\varphi$ for
large sunflowers. If there is no large sunflower at all, we can exactly count
the number of satisfying assignments, using Lemma 5.1. If we do find a large
sunflower, we take its core, add it as a clause to $\psi$, then repeat the
procedure on $\varphi\land\psi$. We will prove after our description of the
algorithm that the answer to the problem is preserved by replacing $\varphi$
with $\varphi\land\psi$.

These clauses are the analogues of the literals $\ell_{i}$ from the proof of
Theorem 4.2 (adding the clause $(\ell_{i})$ to $\varphi$ is the same as the
same as setting $\ell_{i}$ true).

Our procedure returns NO if we find “too many” large sunflowers. Intuitively,
this is equivalent to the fraction of satisfying assignments in $\psi$
becoming “too small” (and if $\Pr[\psi]$ is small, $\Pr[\varphi\land\psi]$
will also be small). Otherwise, the procedure returns YES if
$\varphi\land\psi$ has a small consistent hitting set, since in this case
$\Pr[\varphi\land\psi]\geq\rho$ just by considering assignments which satisfy
the literals in the hitting set.

#### The Pseudocode.

Below we present the pseudocode for the algorithm. We annotate the description
of the algorithm with some comments, indicated by the $\rhd$ symbol, for
additional context and recording changes to $\varphi$ (this formula is not
explicitly used in the algorithm, but is useful to keep around for
bookkeeping). After that, we argue correctness and then discuss the runtime.

  1. 1.

Initialize $F\leftarrow\varphi$.

> _$\rhd$ Initialize $\psi\leftarrow\top$. We maintain throughout that
> $F=\varphi\land\psi$._

Initialize $r_{w}\leftarrow 0$ for all $w\in\\{1,2,\ldots,k-2\\}$.

> _$\rhd$ Here $r_{1}$ counts the number of $1$-sunflowers found so far, and
> for $w>1$, $r_{w}$ counts the number of “relevant” $w$-sunflowers which have
> been added since we last added a $v$-sunflower of weight $v<w$._

  2. 2.

While $r_{w}<t_{w}(\vec{r}[w-1])$ holds for all $w\in\\{1,2,\ldots,k-2\\}$:

> _$\rhd$ Recall that $\vec{r}[w-1]$ is shorthand for $(r_{1},\dots,r_{w-1})$.
> It will turn out that in each pass through the body of this loop, the value
> of $\vec{r}$ becomes lexicographically larger. Consequently, since all the
> $t_{w}(\vec{r}[w-1])$ bounds are constants, the loop is guaranteed to halt
> within $O(1)$ iterations._

    1. (i)

Run the sunflower extraction algorithm from Lemma 5.1 on $F$ with parameter
values $Q_{0}\leftarrow z$ and $Q_{w}\leftarrow q_{w}(\vec{r}[w])$ for $1\leq
w\leq k-2$.

> _$\rhd$ This step either outputs a sunflower or a list of 1-CNFs._

    2. (ii)

If step 22(i) outputs a list of 1-CNFs, use this list to compute $\Pr[F]$
exactly.

If $\Pr[F]\geq\rho$ return YES. Otherwise return NO.

    3. (iii)

If instead step 22(i) outputs a 0-sunflower of size at least $Q_{0}$, return
NO.

    4. (iv)

Otherwise, step 22(i) returns a sunflower $S$ of size at least $Q_{w}$ and
core $C$ of size $|C|=w$.

For every proper subset $D$ of the literals in $C$ in increasing order of
size, let $|D|=v$ and check if $F$ has as $v$-sunflower $T$ of size at least
$Q_{v}$. If any smaller weight sunflower $T$ exists, take such a sunflower-
and-core pair $(T,D)$ which minimizes the size $|D|$, and update $S\leftarrow
T$ and $C\leftarrow D$.

> _$\rhd$ The above check ensures that whenever we add a sunflower of weight
> $w$, none of its literals belong to a large $v$-sunflower for some $v<w$.
> This is useful because it will let us bound the number of times any literal
> appears in $\psi$, which (looking ahead) will help us argue that if we add
> too many sunflowers $\Pr[\psi]$ becomes arbitrarily small. This is the key
> observation that lets us argue that we can run the while loop for $O(1)$
> iterations and still correctly return NO._
> _We describe in the analysis later how to do the above check in linear time,
> using existing FPT set-packing algorithms._
>  _Update $\psi\leftarrow\psi\land C$._

Increment $r_{w}\leftarrow r_{w}+1$ and reset $r_{x}\leftarrow 0$ for all
$x\in[w+1,k-2]$.

Let $F^{\prime}$ be the formula obtained by removing every clause of $F$ which
contains $C$ as as subclause. Update $F\leftarrow F^{\prime}\land C$.

> _$\rhd$ This last step corresponds to asserting that $C$ is true in $F$._

  3. 3.

If $\rho=(1/2)^{t_{1}}$ and the formula $F$ is just a conjunction of a
consistent set of $t_{1}$ literals, return YES.

Otherwise, return NO.

> _$\rhd$ Note that $\rho\geq(1/2)^{t_{1}}$ by definition._

This completes the description of our algorithm. We now prove correctness, by
bounding by the fraction of satisfying assignments $\Pr[\varphi]$ via
conditioning on whether $\psi$ is satisfied or not. We first consider the case
where the algorithm returns an answer during some iteration of the loop in
step 2.

In each iteration of the loop that completes without halting, we find some
clause $C$. We then update $F$ by asserting that $C$ is true, and update
$\psi$ by adding it as a clause to $C$. Because this is the only way these
formulas are modified, we see that in the algorithm above, at the beginning of
any loop iteration the set of satisfying assignments of $F$ is the same as the
set of satisfying assignments of $\varphi\land\psi$. By construction, $\psi$
is a $(k-2)$-CNF with $r_{1}$ distinct clauses of width $1$, and at least
$r_{w}$ distinct clauses of width $w$ for each $w\geq 2$ (there may be more
clauses of width greater than $1$, because of the reset procedure at the end
of step 22(iv)).

Because each clause added to $\psi$ is the core of a large sunflower in $F$,
it turns out that among assignments which do not satisfy $\psi$, the fraction
which do satisfy $\varphi$ is extremely small. We show the following.

######  Claim 5.3.

We have

$\Pr[\varphi\land\lnot\psi]<\min(\alpha,\beta).$

Recall that $\alpha$ and $\beta$ are probability thresholds defined according
to eq. 5 and eq. 6 in the parameters section. This claim is the analogue of
4.9 from the proof of Theorem 4.2. We actually show the claim follows from a
more general result that will be useful later.

######  Claim 5.4.

For each clause of $C$ of $\psi$, let $S(C)$ be the sunflower it came from.
Let $w(C)=|C|$ be the weight of this sunflower and $q(C)=|S(C)|$ be the size
of this sunflower. We also define $\vec{r}(C)=(r_{1}(C),\dots,r_{k-2}(C))$ to
be the particular value taken by variable $\vec{r}$ at the time clause $C$ was
added to the algorithm.

If $\gamma$ is a real number such that

$\left(1-\frac{1}{2^{k-w(C)}}\right)^{q(C)}<\frac{\gamma}{(k-2)T_{w}\cdot
t_{w}(r_{1}(C),\dots,r_{w-1}(C))}$

for every clause $C$ in $\psi$, then we have

$\Pr[\varphi\land\lnot\psi]<\gamma$

as well.

###### Proof.

To prove the above inequality, write $\psi=C_{1}\land C_{2}\land\cdots\land
C_{s}$ as a conjunction of clauses $C_{i}$. Now define the formulas

$D_{i}=\left(\bigwedge_{j<i}C_{j}\right)\land\lnot C_{i}$

for each index $1\leq i\leq s$.

Note that no two of the $D_{i}$ can be satisfied simultaneously. Then by the
law of total probability we have

$\displaystyle\Pr[\varphi\land\lnot\psi]=\Pr[\varphi\land\lnot\psi\land
D_{1}]+\dots+\Pr[\varphi\land\lnot\psi\land
D_{s}]+\Pr[\varphi\land\lnot\psi\land\lnot\left(D_{1}\lor\dots\lor
D_{s}\right)].$ (8)

Observe that $\lnot\psi$ is satisfied precisely when one of the clauses
$C_{i}$ is false. Consequently $\lnot\psi$ is satisfied if and only if one of
the $D_{i}$ is satisfied.

Therefore the final term in (8) vanishes and we can simplify the equation to

$\displaystyle\Pr[\varphi\land\lnot\psi]=\Pr[\varphi\land
D_{1}]+\Pr[\varphi\land D_{2}]+\dots+\Pr[\varphi\land D_{s}].$ (9)

If an assignment $A$ satisfies $D_{i}$, then for $A$ to satisfy $\varphi$ as
well, $A$ must satisfy the variable disjoint set of clauses formed by taking
the sunflower $S(C_{i})$ and removing the core $C_{i}$ from each clause (this
is because for $D_{i}$ to be satisfied, the cores $C_{j}$ for $j<i$ must be
satisfied, while $C_{i}$ is not). Because $S(C_{i})$ came from a $k$-CNF, the
width of its clauses is at most $k-w(C_{i})$, and the probability of
satisfying this variable disjoint set is bounded above by

$\left(1-\frac{1}{2^{k-w(C_{i})}}\right)^{q(C_{i})}<\frac{\gamma}{(k-2)T_{w}\cdot
t_{w}(r_{1}(C_{i}),\dots,r_{w-1}(C_{i}))},$

where the inequality holds due to the hypothesis of the claim. So by
Proposition 2.4 we have

$\Pr[\varphi\land D_{i}]<\frac{\gamma}{(k-2)T_{w}\cdot
t_{w}(r_{1}(C_{i}),\dots,r_{w-1}(C_{i}))}$ (10)

for each index $i$.

Now that we have upper bounds for each of the terms on the right hand side of
eq. 8, we will combine these bounds to get an upper bound on the overall
probability $\Pr[\varphi\land\psi].$

For each integer $1\leq w\leq k-2$ and possible value of
$\vec{r}[w-1]=(r_{1},\dots,r_{w-1})$ which could show up in our algorithm, let
$\mathcal{C}_{w}(\vec{r}[w-1])$ be the set of $w$-clauses $C$ in $\psi$ such
that $r_{1}(C)=r_{1}$, $r_{2}(C)=r_{2}$, …, and $r_{w-1}(C)=r_{w-1}$. The loop
predicate from step 2 guarantees that $|\mathcal{C}_{w}(\vec{r}[w-1])|\leq
t_{w}(\vec{r}[w-1])$ for each choice of $w$ and $\vec{r}$ (since if we ever
get $t_{w}(\vec{r}[w-1])$ clauses of width $w$ for the given values of
$r_{1},\dots,r_{w-1}$, the algorithm will halt). Consequently, by grouping
terms on the right hand side of eq. 9 by the width $w=w(C_{i})$ of the clause
they correspond to, then grouping by their associated values
${r_{1}}(C_{i}),\dots,r_{w-1}(C_{i})$, and then finally applying eq. 10, we
can bound

$\displaystyle\Pr[\varphi\land\lnot\psi]$
$\displaystyle<\sum_{w=1}^{k-2}\sum_{\vec{r}[w-1]}\sum_{C\in\mathcal{C}_{w}(\vec{r}[w-1])}\frac{\gamma}{(k-2)T_{w}\cdot
t_{w}(\vec{r}[w-1])}$
$\displaystyle\leq\sum_{w=1}^{k-2}\sum_{\vec{r}[w-1]}t_{w}(\vec{r}[w-1])\cdot\frac{\gamma}{(k-2)T_{w}\cdot
t_{w}(\vec{r}[w-1])}$
$\displaystyle=\sum_{w=1}^{k-2}\sum_{\vec{r}[w-1]}\frac{\gamma}{(k-2)T_{w}}$
$\displaystyle\leq(k-2)T_{w}\cdot\frac{\gamma}{(k-2)T_{w}}=\gamma.$

Here, the second summation is taken over all $\vec{r}[w-1]$ values satisfying
$0\leq r_{v}\leq t_{v}(\vec{r}[v-1])-1$ for $v\leq w-1$. The inequality from
the first to second line holds because $|\mathcal{C}_{w}(\vec{r}[w-1])|\leq
t_{w}(\vec{r}[w-1])$ from the discussion in the previous paragraph. The
inequality from the third to final line holds because there are $k-2$ choices
for $w$ and at most $T_{w}$ possibilities for $\vec{r}[w-1]$ by definition.

Thus $\Pr[\varphi\land\lnot\psi]<\gamma$, which proves the desired result. ∎

###### Proof of 5.3.

By eq. 7, the hypothesis of 5.4 holds for $\gamma=\min(\alpha,\beta).$ The
result follows. ∎

With these observations, we can prove the correctness of the algorithm. We
first consider the case where the algorithm halts during some iteration of the
loop.

Halting at Step 22(iii)

In this case, since $F$ contains a 0-sunflower of size at least $z$, by
Proposition 2.4 we have

$\Pr[\varphi\land\psi]\leq\left(1-\frac{1}{2^{k}}\right)^{z}<\rho-\alpha.$

Then by eq. 4 and 5.3, we deduce that

$\Pr[\varphi]\leq\Pr[\varphi\land\psi]+\Pr[\varphi\land\lnot\psi]<(\rho-\alpha)+\alpha=\rho$

so we can return NO.

Halting at Step 22(ii)

If $\\#\text{SAT}(F)\geq\rho 2^{n}$, then by eq. 4 we have

$\Pr[\varphi]\geq\Pr[\varphi\land\psi]=\Pr[F]\geq\rho$

and we can return YES.

Otherwise, by Lemma 5.1, the list of $1$-CNFs produced consists of

$m\leq f(z,q_{1}(\vec{r}[1]),q_{2}(\vec{r}[2]),\dots,q_{k-2}(\vec{r}[k-2]))$

formulas for some computable function $f$. Then by Proposition 2.5 and the
case assumption, the number of satisfying assignments $N=\\#\text{SAT}(F)$ is
a sum of at most $m$ powers of two with

$N<\rho 2^{n}.$

Therefore by Lemma 4.6 we have

$\Pr[F]=\Pr[\varphi\land\psi]=\frac{N}{2^{n}}\leq\rho-\eta$ (11)

for some positive $\eta$ whose value depends only on $m$ and $\rho$.

Now, each clause of width $w$ in $\psi$ came from a $w$-sunflower of size
$q_{w}(\vec{s}[w])$ for some

$\vec{s}=(s_{1},\dots,s_{k-2}),$

with the property that its prefix

$\vec{s}[w]=(s_{1},\dots,s_{w})$

is lexicographically smaller than the prefix $\vec{r}[w]=(r_{1},\dots,r_{w})$.
This lexicographical ordering property holds because of how the entries of
$\vec{r}$ are updated in step 22(iv) (namely, when we increment $r_{w}$, we
reset all $r_{x}$ to $0$, for all $x>w$). So if we set parameters so that for
all such $\vec{s}$ we have

$\left(1-\frac{1}{2^{k-w}}\right)^{q_{w}(\vec{s}[w])}<\frac{\eta}{(k-2)T_{w}\cdot
t_{w}(\vec{s}[w-1])}$ (12)

then 5.4 implies that

$\Pr[\varphi\land\lnot\psi]<\eta.$

We can ensure that eq. 12 holds just by setting the $q_{w}(\vec{s}[w])$ to be
sufficiently large in terms of the $q_{w}(\vec{r}[w])$ for all $\vec{r}$
lexicographically after $\vec{s}$. This lexicographical order ensures that we
can satisfy these inequalities while not getting any cyclic dependencies
between constants (in fact, this is exactly why we had the parameters $q_{w}$
depend on the number of $v$-sunflowers found for $v<w$).

Combining the above inequality with eq. 4 and eq. 11 implies that

$\Pr[\varphi]\leq\Pr[\varphi\land\psi]+\Pr[\varphi\land\lnot\psi]<(\rho-\eta)+\eta=\rho$

so we can return NO.

In the remainder of the proof, we show the algorithm is correct when it halts
outside the loop in step 3.

As noted in the comments for the algorithm, in each pass through the loop, the
value of $\vec{r}$ lexicographically increases. Because each entry of
$\vec{r}$ is bounded above by some constant it must be the case that the loop
runs for at most $O(1)$ iterations. So suppose the algorithm completes the
loop without halting. There are two ways this could happen.

First, it could be the case that we set $r_{1}=t_{1}$, meaning we found a set
of $t_{1}$ large 1-sunflowers. In this case, either the cores of the
sunflowers form a small hitting set for the clauses of $\varphi\land\psi$,
which lets us argue that we can return YES, or we can extract a simple
subformula whose fraction of satisfying assignments is strictly less than
$\rho$ (as in the final case in the proof of Theorem 4.2) and we can return
NO.

The other possibility is that the loop terminated because we set
$r_{w}=t_{w}(\vec{r}[w-1])$ for some $w\geq 2$. In this case, we stopped
because we have many large $w$-sunflowers. The analysis for this case is much
trickier, and involves arguing that the structure of $\psi$ and its large
number of clauses forces it to satisfy $\Pr[\psi]<\rho$. Then by eq. 4 we can
return NO in this case.

We now show that the algorithm behaves correctly in these two cases (i.e. we
prove that if the algorithm halts at step 3 it returns the correct answer).

Many 1-Sunflowers: $r_{1}=t_{1}$

Suppose we exit the loop because we set $r_{1}=t_{1}$. In this case, $F$
contains at least $t_{1}$ distinct clauses with just one literal each
(corresponding to the 1-clauses in $\psi$). Let $L$ be the set of literals
among these 1-clauses of $\psi$.

Consider first the case that there is a consistent set $S$ of $t_{1}$ literals
hitting every clause. Then we claim that $S=L$ is forced, so that the hitting
set is made up of precisely the literals appearing as 1-clauses in $\psi$. In
fact, we must have $F=\psi$ and the formulas are completely equal. This is
because after a clause consisting of a single literal $\ell$ is added, we
assert $\ell$ is true in $F$, so all other clauses with $\ell$ disappear from
$F$ and no future clauses with $\ell$ can ever be added.

In this case we have

$\Pr[F]=\Pr[\varphi\land\psi]=(1/2)^{t_{1}}.$

If $\rho=(1/2)^{t_{1}}$ we can return YES, and if $\rho>(1/2)^{t_{1}}$ we can
return NO.

Otherwise, if there is no consistent set of $t_{1}$ literals hitting every
clause, it means that either the set of literals $L$ appearing in the
1-clauses of $\psi$ are not consistent, or it means that $F$ has a clause that
does not contain any literal from $L$.

In the first case we just have $\Pr[F]=\Pr[\varphi\land\psi]=0$, so since
$\Pr[\varphi\land\lnot\psi]<\alpha<\rho$ by 5.3, we have $\Pr[\varphi]<\rho$
by eq. 4 which means we can return NO.

In the second case, consider the subformula formed by taking the 1-clauses in
$\psi$ together with an extra clause of $F$ that shares no literals with them.
Then the fraction of satisfying assignments in this subformula is at most

$\frac{1}{2^{t_{1}}}\cdot\left(1-\frac{1}{2^{k}}\right)=\rho-\beta.$

Then by Proposition 2.4 we deduce that

$\Pr[\varphi\land\psi]\leq\rho-\beta.$

Combining this with 5.3 and eq. 4 as before we deduce that

$\Pr[\varphi]\leq\Pr[\varphi\land\psi]+\Pr[\varphi\land\lnot\psi]<(\rho-\beta)+\beta=\rho$

so we can return NO.

Many Larger Weight Sunflowers

If the algorithm never set $r_{1}=t_{1}$, then it must have exited the loop
because it set $r_{w}=t_{w}(\vec{r}[w-1])$ for some weight $w>1$.

So $\psi$ contains at least $t_{w}(\vec{r}[w-1])$ distinct clauses of width
$w$, and we ended with setting values for $\vec{r}$ such that $r_{v}\leq
t_{v}(\vec{r})-1$ for $v<w$.

Define $\psi^{\prime}$ to be the subformula of $\psi$ formed by the last
$r_{w}=t_{w}(\vec{r}[w-1])$ clauses of width $w$ which were added to the
formula. By the rule for updating the entries of $\vec{r}$ at the end of step
item 2item 2(iv), we know that for all $v<w$, any $v$-clause that ended up in
$\psi$ must have been added before any of the clauses of $\psi^{\prime}$ were
added to $\psi$.

Our goal is to show that $\Pr[\psi^{\prime}]<\rho-\alpha$. Provided this is
true, by Proposition 2.4 we have

$\Pr[\varphi\land\psi]<\Pr[\psi]\leq\Pr[\psi^{\prime}]<\rho-\alpha$

which we can then combine with 5.3 and eq. 4 to deduce that

$\Pr[\varphi]\leq\Pr[\varphi\land\psi]+\Pr[\varphi\land\lnot\psi]<(\rho-\alpha)+\alpha=\rho$

so that returning NO is correct.

To show that $\Pr[\psi^{\prime}]<\rho-\alpha$, we argue in three steps. First,
we show that $\psi^{\prime}$ has no large sunflowers of weight less than $w$.
Second, we use the absence of large sunflowers to argue that each literal
appears at most a bounded number of times in $\psi^{\prime}$. Finally, we use
this last property to prove that $\psi^{\prime}$ contains a large variable
disjoint set, which forces $\Pr[\psi^{\prime}]$ to be small. Intuitively, our
approach is a sort of reverse sunflower extraction argument. Whereas
previously we used Lemma 5.1 to argue that if a formula has no small disjoint
set it must have a large sunflower, we will now prove that if a formula has no
small sunflowers it must have a large disjoint set.

Throughout the remainder of the proof, we let $\vec{r}$ be the vector storing
the final settings of $r_{v}$ after exiting the loop from 2 of the algorithm,
and for convenience write $Q_{v}=q_{v}(\vec{r}[v])$.

######  Claim 5.5.

The formula $\psi^{\prime}$ has no $v$-sunflower of size $Q_{v}$ for any
$v\leq w-1$.

###### Proof.

Intuitively, this result holds because in step 22(iv), before we add the core
of a $w$-sunflower to $\psi$, we first check that none o the literals of the
core belong to a large $v$-sunflower for any $v<w$.

Suppose to the contrary that $\psi^{\prime}$ has a $v$-sunflower of size
$Q_{v}$. Let $C_{1},C_{2},\dots,C_{Q_{v}}$ be the clauses of this
$v$-sunflower, where $C_{1}$ is the clause that was most recently added to
$\psi^{\prime}$. Just before $C_{1}$ was added, the clauses
$C_{2},\dots,C_{Q_{v}}$ were all clauses of $F$. Moreover, $F$ had a
$w$-sunflower, call it $S_{1}$, of size $q_{w}(r_{1},r_{2},\dots,r_{w-1},s)$
for some $s\leq r_{w}$, with core $C_{1}$.

By definition, each clause in $S_{1}$ is of the form $C_{1}\lor D$ where $D$
is a clause of width at most $k-w$. Removing $C_{1}$ from each clause of
$S_{1}$, the result is a variable disjoint set. In particular, ignoring the
literals appearing in the core $C_{1}$, each variable of the formula appears
at most once among the literals in $S_{1}$.

There at most $2w(Q_{v}-1)$ literals which share a variable with some clause
from $C_{2},\dots,C_{Q_{v}}$, since each clause has width $w$. Consequently,
by the above discussion, if $S_{1}$ has at least $2w(Q_{v}-1)+1$ clauses, it
will contain a clause of the form $C^{\prime}=C_{1}\lor D$ such that $D$
shares no variables with any of $C_{2},\dots,C_{Q_{v}}$. Since $C_{1}$ forms a
$v$-sunflower with $C_{2},\dots,C_{Q_{v}}$, we deduce that
$C^{\prime},C_{2},\dots,C_{Q_{v}}$ also form a $v$-sunflower.

Consequently, if $S_{1}$ has size at least $2w(Q_{v}-1)+1$, then there will be
some clause $C_{1}^{\prime}$ in $S_{1}$ with the property that
$C_{1}^{\prime}$ together with $C_{2},\dots,C_{Q_{v}}$ forms a $v$-sunflower
(this is because the latter $Q_{v}-1$ clauses together account for at most
$2w(Q_{v}-1)$ “bad literals” that a clause of $S_{1}$ would need to avoid to
be able to add on to the $v$-sunflower).

We can ensure that $S_{1}$ has size at least $2w(Q_{v}-1)+1$ by taking
$q_{w}(r_{1},r_{2},\dots,r_{w-1},s)$ for any choice of $s$ to be large enough
in terms of $q_{v}(\vec{r}[v])$ for all $v<w$. This can be done, for example,
by taking

$q_{w}(r_{1},r_{2},\dots,r_{w-1},t_{w}(\vec{r}[w-1]))>2w\left(q_{v}(r_{1},\dots,r_{v})-1\right)+1$

for all $v<1$ and make sure that

$q_{w}(r_{1},r_{2},\dots,r_{w-1},0)>q_{w}(r_{1},r_{2},\dots,r_{w-1},1)>\dots$

is a decreasing sequence in the final argument.

Given this condition, we see that some of the literals of $C_{1}$ belong to a
$v$-sunflower of size at least $Q_{v}$. However, if this were true, the check
in step 22(iv) would have found this $v$-sunflower, and then we would not have
added $C_{1}$ (instead, we would have added some smaller weight sunflower). So
this contradicts the behavior of the algorithm, and $\psi^{\prime}$ has no
$v$-sunflower of size $Q_{v}$ as claimed. ∎

######  Claim 5.6.

No literal appears more than

$(w-1)!\cdot 2^{w-1}\prod_{k=1}^{w-1}\left(Q_{k}-1\right)$

times in $\psi^{\prime}$.

###### Proof.

We show that more generally, this claim holds for a $w$-CNF $\psi^{\prime}$
with $2\leq w\leq k-1$ provided $\psi^{\prime}$ satisfies the conclusion of
5.5. We induct on $w$, using similar arguments to the proof of the classical
sunflower lemma [ER60].

First consider the base case of $w=2$. Take any literal $\ell$ in
$\psi^{\prime}$. Let $S$ be the set of clauses which contain $\ell$. If we
remove $\ell$ from each clause of $S$, we get a 1-CNF $S_{\ell}$ of distinct
clauses (if two of the clauses were equal, then $\psi^{\prime}$ would have
duplicate clauses, but this cannot occur because the algorithm never adds the
same sunflower core twice).

Since each variable can only be represented twice in $S_{\ell}$ (as a literal
and its negation), if this set of clauses has size at least $|S_{\ell}|\geq
2(Q_{1}-1)+1$ then $S_{\ell}$ has a variable disjoint set of size at least
$Q_{1}$. But the size of $S_{\ell}$ is just the number of appearances of
$\ell$ in $\psi^{\prime}$. If we add $\ell$ back into these clauses, we
recover a 1-sunflower of size $Q_{1}$ in $S$, and thus $\psi^{\prime}$. But
this contradicts the condition from 5.6 that the formula has no 1-sunflower of
size at least $Q_{1}$. Thus $\ell$ appears at most $2(Q_{1}-1)$ times, which
proves the base case.

Now, take some integer $w\leq k-2$ with $w>2$. For the inductive step, we
assume that the result holds for $(w-1)$-CNF formulas, and prove it must hold
for $w$-CNF formulas $\varphi^{\prime}$ as well.

As before, take an arbitrary literal $\ell$, let $S$ be the set of clauses
containing $\ell$, and let $S_{\ell}$ be the set formed by removing $\ell$
from each clause of $S$. The formula $S_{\ell}$ is a $(w-1)$-CNF on distinct
clauses. Moreover, a $v$-sunflower in $S_{\ell}$ corresponds to a
$(v+1)$-sunflower in $S$ (by adding the literal $\ell$ to the core).
Consequently, since we assume that $\psi^{\prime}$ satisfies the conclusion of
5.5, we know that $S_{\ell}$ has no 1-sunflower of size $Q_{2}$, no
2-sunflower of size $Q_{3}$, etc. Thus by the inductive hypothesis we get that
any literal appears at most $P=(w-2)!\cdot
2^{w-2}\prod_{k=2}^{w-1}\left(Q_{k}-1\right)$ times in $S_{\ell}$.

Take a maximal variable disjoint set $D$ of clauses from $S_{\ell}$. By
maximality, every clause in $S_{\ell}$ shares some variable with a clause from
$D$. Since each clause in $D$ has width at most $w-1$ and each literal appears
in $S_{\ell}$ at most $P$ times, each clause of $D$ shares a variable with at
most $2(w-1)P$ clauses in $S_{\ell}$. This means that

$|S_{\ell}|\leq 2(w-1)P\cdot|D|.$

Now, the clauses in $D$ form a 0-sunflower in $S_{\ell}$. Adding the literal
$\ell$ back into these clauses forms a 1-sunflower of size $|D|$ in $S$. By
assumption, $S$ has no 1-sunflower of size $Q_{1}$. Thus $|D|\leq Q_{1}-1$.
Substituting this bound into the above inequality, we deduce that

$|S_{\ell}|\leq 2(w-1)P\cdot(Q_{1}-1)=(w-1)!\cdot
2^{w-1}\prod_{k=1}^{w-1}\left(Q_{k}-1\right).$

However, the size of $S_{\ell}$ is just the number of times $\ell$ appears in
$\psi^{\prime}$. So $\ell$ appears at most

$(w-1)!\cdot 2^{w-1}\prod_{k=1}^{w-1}\left(Q_{k}-1\right)$

times in $\psi^{\prime}$, which completes the induction and proves the desired
result. ∎

Using 5.6, we now show that for the appropriate choice of parameters,
$\psi^{\prime}$ will have a large variable disjoint set. Set
$t_{w}(\vec{r}[w-1])$ large enough that

$\left(1-\frac{1}{2^{w}}\right)^{\lceil
t_{w}(\vec{r}[w-1])/\left(2w\cdot(w-1)!2^{w-1}\prod_{k=1}^{w-1}\left(Q_{k}-1\right)\right)\rceil}<\rho-\alpha$
(13)

for all possible values for the $Q_{k}$ as described above. We can do this by
setting $t_{w}(\vec{r}[w-1])$ large enough in terms of all
$q_{v}(r_{1},\dots,r_{v})$ values for $v<w$ (and then once we set this
$t_{w}(\vec{r})$ value we can set values for the corresponding $q_{w}$
constants). This is valid, because $t_{w}$ depends on the numbers of
$v$-sunflowers found for $v<w$ (so we do not have any cyclic dependencies
among parameters in this step).

By applying 5.6 and picking clauses greedily, we see that the formula
$\psi^{\prime}$ must have a variable disjoint set of size at least

$\left\lceil\frac{t_{w}(\vec{r}[w-1])}{\left(2w\cdot(w-1)!\cdot
2^{w-1}\prod_{k=1}^{w-1}\left(Q_{k}-1\right)\right)}\right\rceil.$

Then by our choice in eq. 13 and proposition 2.4 we get

$\Pr[\psi^{\prime}]<\rho-\alpha.$

The previous discussion then implies that we can return NO.

This completes the proof of correctness for the entire algorithm. It remains
to check the runtime.

As mentioned before, the loop runs for at most a constant number of
iterations. In each iteration, we may use the sunflower extraction algorithm
of Lemma 5.1, scan through the clauses of a formula to remove clauses which
have a particular subclause, and check whether a particular clause has
literals belonging to a $v$-sunflower of some size $Q$.

The proof of Lemma 5.1 shows that calling the sunflower extraction algorithm
takes linear time for constant $k$ and constant sized parameters (and all our
parameters are constant, since $k$ is constant and $\rho$ has bounded
denominator). We can certainly remove all clauses which have a particular
subclause in linear time, since this just takes a constant amount of work for
each clause in the formula. Finally, to check whether a particular clause has
literals belonging to a $v$-sunflower of some size $Q$, we check at most
$2^{k}$ subsets of literals. For each such subset, we can perform the check by
considering the set of clauses containing these literals, removing this subset
of literals from each clause, and then checking if there exists a variable
disjoint set of size at least $Q$ among the resulting clauses.

This last problem, of finding some number of pairwise disjoint sets from a
family of subsets, is referred to as the _(Disjoint) Set Packing_ problem in
the literature. Our algorithm needs to solve a Set Packing instance where each
set has size at most $k$ and we are looking for at least $Q$ mutually disjoint
sets. Directly applying known fixed-parameter tractable algorithms for
Disjoint Set Packing, such as the algorithm from [JZC04] for example, this can
be done in linear time for constant $k$ and $Q$.

Thus the algorithm runs in linear time as claimed. ∎

###  5.1 Computing the Higher-Order Bits of #$k$SAT

As a simple consequence of our threshold SAT algorithm, we observe that for
any $k$-CNF we can compute the “higher order bits” of the number of satisfying
assignments in polynomial time. More precisely, given an integer
$N\in[0,2^{n}]$, it has a unique binary representation of the form

$N=\sum_{j=0}^{n}b_{j}2^{n-j}$

for some binary digits $b_{j}\in\left\\{0,1\right\\}$. Given any integer $t$,
the first $t+1$ of these digits $b_{0},\dots,b_{t}$ are said to be the $t+1$
_most significant bits_ of $N$.

######  Corollary 5.7.

For any positive integers $k$ and $t$, and a $k$-CNF $\varphi$, we can compute
the $t+1$ most significant bits of $\\#\text{SAT}(\varphi)$ in
$O_{k,t}(|\varphi|)$ time.

###### Proof.

Let the number of satisfying assignments of $\varphi$ have binary
representation

$\\#\text{SAT}(\varphi)=\sum_{j=0}^{n}b_{j}2^{n-j}.$ (14)

First, we check if $\varphi$ is empty or not. If it is empty, then
$\varphi=\top$ is a tautology, so $\\#\text{SAT}(\varphi)=2^{n}$ and we can
just return $b_{0}=1$ and $b_{1}=\dots=b_{t}=0$ to get all $t+1$ most
significant bits of $\\#\text{SAT}(\varphi)$.

Otherwise $\varphi$ is not always true, so $\\#\text{SAT}(\varphi)<2^{n}$ and
$b_{0}=0$.

We now run the following procedure for stages $i=1,\dots,t$. Each stage
determines the $i$-th higher-order bit. At the beginning of stage $i$, we
assume we have already computed $b_{0},\dots,b_{i-1}$ and that $b_{0}=0$. Set

$\rho_{i}=\frac{1}{2^{i}}+\sum_{j=1}^{i-1}\frac{b_{j}}{2^{j}}.$

Then $\rho_{i}$ can be written as a rational with denominator at most
$2^{i}\leq 2^{t}$. So by Theorem 5.2, we can solve THR${}_{\rho_{i}}$-$k$SAT
on $\varphi$ in $O_{k,t}(|\varphi|)$ time.

If we find that $\\#\text{SAT}(\varphi)\geq\rho 2^{n}$, then we set $b_{i}=1$.
Otherwise we set $b_{i}=0$. We then proceed to the next stage. After stage $t$
terminates, we return the values $b_{0},\dots,b_{t}$ computed.

This procedure is correct by a simple induction on the stage number $i$. We
already computed $b_{0}$ at the beginning.

Suppose at the beginning of stage $i$ we have correctly found the $i$ most
significant digits $b_{0},\dots,b_{i-1}$ of the total count satisfying
assignments $\\#\text{SAT}(\varphi)$. Then if $b_{i}=1$, by eq. 14 we have

$\\#\text{SAT}(\varphi)\geq\sum_{j=0}^{i}b_{j}2^{n-j}=\left(\frac{1}{2^{i}}+\sum_{j=0}^{i-1}\frac{b_{j}}{2^{j}}\right)2^{n}=\rho_{i}2^{n}$

so $\varphi$ is as YES instance for THR${}_{\rho_{i}}$-$k$SAT. Similarly, if
$b_{i}=0$, by eq. 14 we have

$\\#\text{SAT}(\varphi)=\left(\sum_{j=0}^{i-1}\frac{b_{j}}{2^{j}}+\sum_{j=i+1}^{n}\frac{b_{j}}{2^{j}}\right)2^{n}<\left(\sum_{j=0}^{i-1}\frac{b_{j}}{2^{j}}+\sum_{j=i+1}^{\infty}\frac{1}{2^{j}}\right)2^{n}=\left(\sum_{j=0}^{i-1}\frac{b_{j}}{2^{j}}+\frac{1}{2^{i}}\right)2^{n}=\rho_{i}2^{n}$

so $\varphi$ is a NO instance for THR${}_{\rho_{i}}$-$k$SAT.

Thus at each stage $i$, our algorithm correctly computes the next most
significant bit of $\\#\text{SAT}(\varphi)$. So by induction at the end of $t$
stage we will have correctly computed the $t+1$ most significant bits of the
number of satisfying assignments in $\varphi$ as claimed. The claimed runtime
bound holds because we make $t+1$ calls to routines taking
$O_{k,t}(|\varphi|)$ time per call. ∎

##  6 The Complexity of Inference Problems over k-CNFs

In this section we explain how our algorithms for MAJORITY-$k$SAT have
interesting implications for the more general inference problems discussed in
Section 1.1.

###  6.1 E-MAJ-$k$SAT

For reference, we recall the definition of E-MAJ-SAT, stated slightly
differently for this section:

> E-MAJ-SAT: Given a CNF $F$ over $n+n^{\prime}$ variables
> $\vec{x}=x_{1},\ldots,x_{n}$ and $\vec{y}=y_{1},\ldots,y_{n^{\prime}}$,
> determine if there is an assignment $A$ to the $\vec{x}$-variables such that
> $F(A,\vec{y})$ has at least $2^{n^{\prime}-1}$ satisfying assignments.

In the context of E-MAJ-SAT, we say the $\vec{x}$ are _existential variables_
and the $\vec{y}$ are _probabilistic variables_. Observe that when $n=0$,
E-MAJ-SAT is equivalent to MAJORITY-SAT.

Our first result generalizes the Theorem 3.1 showing MAJORITY-$2$SAT
$\in\mathsf{P}$, to prove that E-MAJ-$2$SAT is in $\mathsf{P}$. In fact a
slightly more general result holds.

######  Theorem 6.1.

E-MAJ-$2$SAT $\in\mathsf{P}$. In particular, for every $\rho\in(0,1)$, we can
determine in $n^{O(\log(1/\rho))}$ time whether there is an assignment to the
existential variables such that at least a $\rho$-fraction of the assignments
to probabilistic variables are satisfying.

###### Proof.

Let $\rho\in(0,1)$. We are given a $2$-CNF $F(\vec{x},\vec{y})$ with
existential variables $\vec{x}=x_{1},\ldots,x_{n}$ and probabilistic variables
$\vec{y}=y_{1},\ldots,y_{n^{\prime}}$, and wish to know if there is an
assignment $A$ to $\vec{x}$ such that at least a $\rho$-fraction of the
possible assignments to $\vec{y}$ satisfies $F(A,\vec{y})$. Call an assignment
$A$ good if it satisfies this property.

For brevity, in the following we will refer to a “$\vec{y}$-variable” as a
variable $y_{i}$ from $\vec{y}$, and a “$\vec{y}$-literal” as a literal
($y_{i}$ or $\neg y_{i}$) from $\vec{y}$.

We partition the $2$-clauses of $F$ into three sets. $P_{x}$ contains those
clauses with two $x_{i}$ variables, $P_{x,y}$ contains those clauses with one
$x_{i}$ variable and one $y_{j}$ variable, and $P_{y}$ contains those clauses
with two $y_{j}$ variables.

Over the clauses in $P_{y}$, we find a maximal disjoint set $S$ of clauses,
analogously to Theorem 3.1. If $|S|>1+\log_{4/3}(1/\rho)$, then we can answer
NO, as the subformula $P_{y}$ of $F(A,\vec{y})$ is already satisfied by less
than a $\rho$-fraction of the possible assignments to $\vec{y}$. Otherwise,
$|S|\leq 1+\log_{4/3}(1/\rho)$. By trying all possible satisfying assignments
to the variables of $S$ and arguing as in Theorem 3.1, we can express $P_{y}$
as a decision tree $T_{y}$ of size at most $2^{|S|}\leq\text{poly}(1/\rho)$,
whose inner nodes are labeled with variables from $S$, and whose leaves are
labeled with $1$-CNFs over $\vec{y}$ (the decision tree represents all
assignments over the “hitting set” $S$, and the $1$-CNFs represent the reduced
$2$-CNF formula after the variables in the hitting set are assigned).

Now we consider the $P_{x,y}$ subformula. For any assignment $A$ to the
variables $\vec{x}$, let $L_{A}$ be the set of literals of $\vec{y}$ that are
implied by assigning the $\vec{x}$ variables according to $A$ in $P_{x,y}$
(for example, if $(x_{i}\vee y_{j})$ is a clause of $P_{x,y}$ and $x_{i}$ is
set false in $A$, then $y_{j}$ is put in $L_{A}$). Our task of finding a good
assignment $A$ is thus equivalent to finding an $A$ to the $\vec{x}$ variables
such that the 2-CNF $P_{x}$ is satisfied, and $T_{y}$ conjoined with the set
of $\vec{y}$-literals $L_{A}$ has at least $\rho\cdot 2^{n^{\prime}}$
satisfying assignments.

Observe that for any good assignment $A$ we must have
$|L_{A}|\leq\log_{2}(1/\rho)$, since otherwise the fraction of satisfying
assignments in $F(A,\vec{y})$ is already at most $1/2^{|L_{A}|}<\rho$. Thus it
must be that at most $\log_{2}(1/\rho)$ distinct $\vec{y}$-literals are
implied in $P_{x,y}$ by a good assignment $A$.

Let us guess the set of $\vec{y}$-literals $L^{\star}$ that are implied in
$P_{x,y}$ by a good assignment $A$ to $\vec{x}$. If $F$ is a YES-instance,
then $|L_{A}|\leq\log_{2}(1/\rho)$ and there are only $n^{O(\log(1/\rho))}$
possible guesses for the literals in $L^{\star}$, which we can enumerate one-
by-one. We can verify $L^{\star}$ by doing two checks which connect
$L^{\star}$ to $P_{x}$ and to $P_{y}$, respectively.

  * (a)

First, we check that some assignment $A$ to $\vec{x}$ implies _exactly_ the
literals in $L^{\star}$ to be true in $P_{x,y}$ (no other literals from
$\vec{y}$ are forced in $P_{x,y}$), and $A$ satisfies $P_{x}$.

For every $(\ell_{i}\vee\ell^{\prime}_{j})$ in $P_{x,y}$ where $\ell_{i}$ is a
literal over $\vec{x}$ and $\ell^{\prime}_{j}$ is a $\vec{y}$-literal not in
$L^{\star}$, we must have that $\ell_{i}$ is true according to our guess
(otherwise, $\ell^{\prime}_{j}$ would be forced true, but
$\ell^{\prime}_{j}\notin L^{\star}$). Therefore, we can set true all literals
over $\vec{x}$ variables that appear in clauses with literals of $\vec{y}$
that are not in $L^{\star}$.

After doing so, the clauses $(\ell_{i}\vee\ell^{\prime}_{j})$ remaining in
$P_{x,y}$ are such that $\ell^{\prime}_{j}\in L^{\star}$. As we are guessing
that $\ell^{\prime}_{j}$ is implied true by $A$ in $P_{x,y}$, it must be that
$\ell_{i}$ is false for at least one clause that $\ell^{\prime}_{j}$ appears
in. Thus, for the set of clauses of $P_{x,y}$ containing $\ell^{\prime}_{j}\in
L^{\star}$

$S=\\{(\ell_{1}\vee\ell^{\prime}_{j}),\ldots,(\ell_{t}\vee\ell^{\prime}_{j}),\\}$

we replace $S$ in $P_{x,y}$ with the single long clause

$(\neg\ell_{1}\vee\cdots\vee\neg\ell_{t}).$

This replacement is valid, as we are guessing that $\ell^{\prime}_{j}$ is
implied true in $P_{x,y}$, so at least one of the $\ell_{i}$ must be false
(and each clause in $S$ will be satisfied if $\ell^{\prime}_{j}$ is true). As
$|L^{\star}|\leq\log_{2}(1/\rho)$, at most $\log_{2}(1/\rho)$ such long
clauses are added to $P_{x,y}$.

Finally, enumerating all $n^{O(\log(1/\rho))}$ possible ways to choose one
literal from each of the $(\neg\ell_{1}\vee\cdots\vee\neg\ell_{t})$ clauses
(which every assignment that forces $L^{\star}$ must satisfy), we then check
(in polynomial time) that $P_{x}$ is satisfiable on the remaining $\vec{x}$
variables. If this is true for some assignment to the long clauses, we say the
check _passes_ (otherwise, the check fails, and we try a different
$L^{\star}$).

  * (b)

Second, we check that the number of satisfying assignments to the remaining
subformula $F(A,\vec{y})$ is at least $\rho\cdot 2^{n^{\prime}}$, assuming
$L^{\star}$ is the set of $\vec{y}$-literals implied by $A$ in $F_{x,y}$.

As argued above, this equals the number of satisfying assignments to $T_{y}$
conjoined with $L^{\star}$. To compute this, we conjoin the set of literals
$L^{\star}$ with each of the $1$-CNFs on the leaves of $T_{y}$, then compute
the sum over all leaves $\ell$ in $T_{y}$ of the number of SAT assignments for
the $1$-CNF at leaf $\ell$. Therefore we can compute the $\\#$SAT value in
$O(n)$ time, and verify whether it is at least $\rho\cdot 2^{n^{\prime}}$. If
so, we say that this check _passes_.

Finally, our algorithm outputs YES if and only if both checks pass for some
guessed set $L^{\star}$. This completes the algorithm, and the proof. ∎

Although E-MAJ-$2$SAT turns out to be solvable in polynomial time, we can show
that E-MAJ-$3$SAT is $\mathsf{NP}$-complete.

######  Theorem 6.2.

For all $k\geq 3$, E-MAJ-$k$SAT is $\mathsf{NP}$-complete.

###### Proof.

First, the problem is in $\mathsf{NP}$ for every $k$, because we could guess a
satisfying assignment to the existential variables, plug it in, then determine
whether the remaining formula has a majority (or a $\rho$-fraction, for
constant $\rho$) of satisfying assignments in polynomial time, by Theorem 4.1.

Now we prove $\mathsf{NP}$-hardness. Given a $k$-CNF $F$ on variables
$x_{1},\ldots,x_{n}$, make an E-MAJ-$k$SAT instance
$F^{\prime}=F\wedge(x_{n+1}\vee x_{n+2})$ with $n$ existential variables and
the two probabilistic variables $x_{n+1}$ and $x_{n+2}$. If $F$ is
satisfiable, then there is an assignment to the first $n$ variables of
$F^{\prime}$ such that the probability a random assignment satisfies
$(x_{n+1}\vee x_{n+2})$ is at least $3/4>1/2$. Otherwise, if $F$ is
unsatisfiable, then every assignment to the first $n$ variables leads to a
probability of zero on the remaining formula (the remaining formula is false).
∎

###  6.2 MAJ-MAJ-$k$SAT

Recall the MAJ-MAJ-SAT problem, as defined in the introduction:

> MAJ-MAJ-SAT: _Given $n$, $n^{\prime}$, and a formula $F$ over $n+n^{\prime}$
> variables, do a majority of the assignments to the first $n$ variables of
> $F$ yield a formula where the majority of assignments to the remaining
> $n^{\prime}$ variables are satisfying?_

Since MAJORITY-$k$SAT is in $\mathsf{P}$ for all $k$ (Theorem 1.1), we can
already conclude that MAJ-MAJ-$k$SAT is in ${\mathsf{PP}}$ (a significant
improvement over the obvious ${\mathsf{PP}}^{{\mathsf{PP}}}$ upper bound).
Just as with E-MAJ-$2$SAT, we can say more in the case of $k=2$.

######  Theorem 6.3.

MAJ-MAJ-$2$SAT $\in\mathsf{P}$. Moreover, given a $2$-CNF $F$ and parameters
$\rho,\sigma\in(0,1)$, we can determine if

$\Pr_{a\in\\{0,1\\}^{n}}\left[\Pr_{b\in\\{0,1\\}^{n^{\prime}}}[F(a,b)=1]\geq\sigma\right]\geq\rho$

in $\text{poly}(1/\rho)\cdot n^{O(\log(1/\sigma))}$ time. In fact, when the
algorithm answers YES, it returns the exact number of $a$ such that
$\Pr_{b}[F(a,b)=1]\geq\sigma$.

###### Proof.

We proceed very similarly as the algorithm for E-MAJ-$2$SAT (Theorem 6.1), but
need to make some changes to avoid having to solve the
$\\#\mathsf{P}$-complete $\\#2$SAT problem.

Let $F(\vec{x},\vec{y})$ be a $2$-CNF with variables
$\vec{x}=x_{1},\ldots,x_{n}$ and variables
$\vec{y}=y_{1},\ldots,y_{n^{\prime}}$. Given $\rho,\sigma\in(0,1)$, we wish to
know whether or not

$\Pr_{a\in\\{0,1\\}^{n}}\left[\Pr_{b\in\\{0,1\\}^{n}}[F(a,b)=1]\geq\sigma\right]\geq\rho.$

As in Theorem 6.1, we partition the clauses of $F$ into three sets: $P_{x}$
contains those clauses with two $x_{i}$ variables, $P_{x,y}$ contains those
clauses with one $x_{i}$ variable and one $y_{j}$ variable, and $P_{y}$
contains those clauses with two $y_{j}$ variables.

Over the formula $P_{x}$, we find a maximal disjoint set $S_{x}$ of clauses
(analogously to Theorem 6.1 and Theorem 3), and over $P_{y}$, we find a
maximal disjoint set $S_{y}$ of clauses. If either
$|S_{x}|>1+\log_{4/3}(1/\rho))$ or $|S_{y}|>1+\log_{4/3}(1/\sigma)$, then we
can answer NO. In more detail, this is because in the first case, the
subformula $P_{x}$ of $F(\vec{x},\vec{y})$ is only satisfied by less than a
$\rho$-fraction of the possible assignments $a$ to $\vec{x}$, regardless of
how $\vec{y}$ is set, so the fraction of $a\in\\{0,1\\}^{n^{\prime}}$ such
that $(\exists b)[F(a,b)=1]$ holds is less than $\rho$. Therefore the fraction
of $a$ such that $\Pr_{b}[F(a,b)=1]\geq\sigma$ holds is also less than $\rho$.
In the second case, $P_{y}$ is only satisfied by less than a $\sigma$-faction
of the possible assignments to $\vec{y}$ regardless of how $\vec{x}$ is set.

Otherwise, we have $|S_{x}|\leq 1+\log_{4/3}(1/\rho)$ and $|S_{y}|\leq
1+\log_{4/3}(1/\sigma)$. Enumerating all satisfying assignments to the
variables of $S_{x}$ and $S_{y}$, and arguing as in Theorem 3.1, both $P_{x}$
and $P_{y}$ can be expressed as decision trees $T_{x}$ and $T_{y}$ of a
particular form. $T_{x}$ has size at most $2^{|S_{x}|}\leq\text{poly}(1/\rho)$
with inner nodes labeled by variables from $S_{x}$, and leaves labeled by
$1$-CNFs over the variables $\vec{x}$. $T_{y}$ has size at most
$2^{|S_{y}|}\leq\text{poly}(1/\sigma)$, inner nodes labeled with variables
from $S_{y}$, and leaves labeled by $1$-CNFs over $\vec{y}$.

We have processed the $P_{x}$ and $P_{y}$; now we turn to handling $P_{x,y}$.
As in Theorem 6.1, for any assignment $A$ to the variables $\vec{x}$, let
$L_{A}$ be the set of literals of $\vec{y}$ that are implied by assigning the
$\vec{x}$ variables according to $A$ in $P_{x,y}$. We say that an assignment
$A$ to $\vec{x}$ is good if $\Pr_{b}[F(A,b)=1]\geq\sigma$. We want to
determine whether the fraction of good assignments is at least $\rho$ or not.

For any good assignment $A$, it must be that $|L_{A}|\leq\log_{2}(1/\sigma)$,
since otherwise the fraction of satisfying assignments in $F(A,\vec{y})$ is at
most $1/2^{|L_{A}|}<\sigma$ (so $A$ is not good). Thus there are
$n^{O(\log(1/\sigma))}$ possible choices for the set $L_{A}$ (note that every
good assignment $A$ is associated with exactly one set $L_{A}$: this is
trivial, but important to note for the count of SAT assignments).

For each of these choices $L^{\star}$, we process $P_{y}$ similarly as in
Theorem 6.1. First of all, assuming $L^{\star}$ is the set of literals forced
in $P_{x,y}$, we can determine the exact number of assignments to the
remaining variables of $\vec{y}$ that satisfy $P_{y}$ in $\text{poly}(n)$
time, by asserting the literals of $L^{\star}$ at each leaf of the decision
tree $T_{y}$ and solving $\\#$SAT on the resulting decision tree in
$\text{poly}(1/\sigma)\cdot\text{poly}(n)$ time (this is completely analogous
to what happens in Theorem 6.1). Let $N_{y}(L^{\star})$ be the number of
satisfying assignments obtained.

Given $L^{\star}$, we also set all $\vec{x}$-variables that appear in clauses
of $P_{x,y}$ with $\vec{y}$-literals that are _not_ in $L^{\star}$. For the
literals $\ell\in L^{\star}$, in Theorem 6.1, we derived $|L^{\star}|$ long
clauses over $\vec{x}$ that must to be true in order for $L^{\star}$ to be
correct, and we simply picked one literal from each of these clauses. To get a
proper count of the assignments $a\in\\{0,1\\}^{n}$ such that
$\Pr_{b}[F(a,b)]\geq\sigma$, we have to work a little harder. We will use an
inclusion-exclusion approach, standard in exponential-time algorithmics
[FK10]. In particular, for long clauses $C_{1},\ldots,C_{t}$, we have

$\displaystyle\sum_{a\in\\{0,1\\}^{n}}(T_{x}(a)\wedge
C_{1}(a),\ldots,C_{t}(a))=\sum_{S\subseteq[t]}(-1)^{|S|}\cdot\sum_{a\in\\{0,1\\}^{n}}\left(T_{x}(a)\wedge\bigwedge_{i\in
S}(\neg C_{i}(a))\right).$ (15)

Note the sum on the LHS is only over assignments to the existential variables
$\vec{x}$. In our case, $t=|L^{\star}|\leq O(\log(1/\sigma))$, so the number
of terms on the RHS is only $2^{O(\log(1/\sigma)}\leq\text{poly}(1/\sigma)$.
Each such term asserts a $1$-CNF formula $\bigwedge_{i\in S}(\neg C_{i}(a))$
over the variables $\vec{x}$. As in the case of $T_{y}$ above, we can
enumerate all the assignments to $\vec{x}$ satisfying
$(T_{x}(a)\wedge\bigwedge_{i\in S}(\neg C_{i}(a))$ in
$\text{poly}(1/\rho)\cdot\text{poly}(n)$ time. Let $N_{x}(L^{\star})$ be the
number of assignments obtained by evaluating (15).

Finally, we use these $N_{x}(L^{\star})$ and $N_{y}(L^{\star})$ values to
determine the answer. Let $S_{L^{\star}}$ be the set of good assignments $A$
to $\vec{x}$ such that $P_{x}(A)\wedge P_{x,y}(A)$ evaluates to precisely the
conjunction of all $\vec{y}$-literals in $L^{\star}$. Observe that for
different $\vec{y}$-literal sets $L^{\star}$ and $(L^{\prime})^{\star}$, we
must have $S_{L^{\star}}\cap S_{(L^{\prime})^{\star}}=\emptyset$, and the
union over all $S_{L^{\star}}$ contains all good assignments to $\vec{x}$.
This is because the ones which are not good are those for which $L^{\star}$ is
the set of implied $\vec{y}$-literals, but those implied literals force $F$ to
be false for less than a $\sigma$-fraction of the $\vec{y}$-assignments. We
observe that the condition

$\Pr_{a\in\\{0,1\\}^{n}}\left[\Pr_{b\in\\{0,1\\}^{n}}[F(a,b)=1]\geq\sigma\right]\geq\rho$

is equivalent to the condition

$\displaystyle\sum_{\text{set~{}}L^{\star}:|L^{\star}|\leq
O(\log(1/\sigma)}N_{x}(L^{\star})\cdot[N_{y}(L^{\star})\geq\sigma\cdot
2^{n^{\prime}}]\geq\rho\cdot 2^{n},$ (16)

where $[P]:=1$ if the condition $P$ is true, and is $0$ otherwise. In
particular, the sum in (16) is equivalent to enumerating over all assignments
$A$ to $\vec{x}$ in the union of all $S_{L^{\star}}$, but only counting those
$A$ which result in at least $\sigma\cdot 2^{n^{\prime}}$
$\vec{y}$-assignments being true in $F(A,\vec{y})$. These are precisely the
good assignments of $F$.

Therefore, we can determine YES or NO for our given instance in
$n^{O(\log(1/\rho))}\cdot\text{poly}(1/\rho,n)$ time, by computing the sum on
the LHS of (16). ∎

What is the complexity of MAJ-MAJ-$k$SAT for $k>2$? Our inclination is to
believe that MAJ-MAJ-$k$SAT is in $\mathsf{P}$ for all $k\geq 3$, but have not
yet extended our other algorithms to show this.

##  7 Algorithms and Hardness For Two Variants of MAJORITY-SAT

We have shown surprising positive results for solving MAJORITY-SAT on bounded-
width CNFs. In this section, we prove results on the complexity of natural
variations of MAJORITY-$k$SAT: algorithms and hardness for MAJORITY-$k$SAT
with one arbitrary-width clause, and GtMAJORITY-$k$SAT which asks whether the
number of satisfying assignments to a $k$-CNF is strictly greater than
$\rho\cdot 2^{n}$ for a fraction $\rho\in(0,1)$.

###  7.1 MAJORITY-SAT With One Long Clause

Here, we prove the following theorem from the introduction.

Reminder of Theorem 1.6.  Deciding MAJORITY-SAT over $k$-CNFs with one extra
clause of arbitrary width is in $\mathsf{P}$ for $k=2$, $\mathsf{NP}$-hard for
$k=3$, and ${\mathsf{PP}}$-complete for $k\geq 4$.

We begin with the case of $k\geq 4$.

######  Theorem 7.1.

It is ${\mathsf{PP}}$-complete to determine if a given $k$-CNF $F$ with _one_
arbitrary width clause and $n$ variables has $\\#\text{SAT}(F)\geq 2^{n-1}$,
for all $k\geq 4$.

###### Proof.

Verifying that the problem is in ${\mathsf{PP}}$ is straightforward. To prove
${\mathsf{PP}}$-hardness, suppose we are given a parameter
$t\in\\{1,\ldots,n\\}$ and a $3$-CNF formula $F=C_{1}\wedge\cdots\wedge C_{m}$
on $n$ variables (where $n$ is even) and want to know if $\\#\text{SAT}(F)\geq
2^{n-t}$ or not. Bailey-Dalmau-Koliatis [BDK07] show this problem is
${\mathsf{PP}}$-complete.

Introduce new variables $x_{n+1},y_{1},\ldots,y_{t}$, and consider the formula

$F^{\prime}=(x_{n+1}\vee C_{1})\wedge\cdots\wedge(x_{n+1}\vee
C_{m})\wedge(\neg x_{n+1}\vee y_{1}\vee\cdots\vee y_{t}).$

Observe that $F^{\prime}$ is $4$-CNF with the exception of one clause of
length $t+1$. Considering the cases where $x_{n+1}$ is false and $x_{n+1}$ is
true, we have

$\\#\text{SAT}(F^{\prime})=2^{t}\cdot\\#\text{SAT}(F)+2^{n+t}\cdot(1-1/2^{t}).$

As a fraction of all possible assignments, this is

$\rho=\\#\text{SAT}(F)/2^{n+1}+1/2-1/2^{t+1}.$

Observe that $\\#\text{SAT}(F)\geq 2^{n-t}$ if and only if

$\rho\geq 1/2+2^{n-t}/2^{n+1}-1/2^{t+1}=1/2.$

Therefore $F^{\prime}$ is an instance of MAJORITY-SAT if and only if
$\\#\text{SAT}(F)\geq 2^{n-t}$. ∎

Next, we show that MAJORITY-SAT over $3$-CNFs with one long clause is
$\mathsf{NP}$-hard.

######  Theorem 7.2.

If we can determine whether a given $3$-CNF $F$ with one arbitrary-width
clause and $n$ variables satisfies $\\#\text{SAT}(F)\geq 2^{n-1}$ in
polynomial time, then $\mathsf{P}=\mathsf{NP}$.

###### Proof.

Using the same reduction as in Theorem 7.1, given any $2$-CNF $F$ and integer
$t$, we can reduce the problem of determining whether $\\#\text{SAT}(F)\geq
2^{t}$ to determining whether a given $3$-CNF $F^{\prime}$ with one long
clause has $\\#\text{SAT}(F^{\prime})\geq 2^{n-1}$. Therefore, if there were a
polynomial-time algorithm for determining $\\#\text{SAT}(F^{\prime})\geq
2^{n-1}$, there would also be a polynomial-time algorithm for determining
whether $\\#\text{SAT}(F^{\prime})\geq 2^{t}$ or not, for $2$-CNF formulas.

Making $O(\log n)$ calls to such a polynomial-time algorithm (until we find a
$t$ such that $\\#\text{SAT}(F^{\prime})\geq 2^{t}$ but
$\\#\text{SAT}(F^{\prime})<2^{t+1}$), we can approximate the number of
satisfying assignments to any $2$-CNF, within a factor of $2$. However, this
problem is $\mathsf{NP}$-hard (see for example Theorem 4.1 in [Zuc96]).

∎

It seems the following problem is probably ${\mathsf{PP}}$-complete:

> Given a $2$-CNF $F^{\prime}$ and integer $t$, decide whether
> $\\#\text{SAT}(F)\geq 2^{t}$.

If so, the above hardness result can be improved to
${\mathsf{PP}}$-hardness.111111The difficulty with directly using the fact
that $\\#2$SAT is $\\#\mathsf{P}$-hard [Val79] is that all proofs we know that
reduce from $\\#3$SAT to $\\#2$SAT significantly alter the number of
satisfying assignments. So, a reduction from the 3-CNF version to the 2-CNF
version is not immediate.

Nevertheless, MAJORITY-$2$SAT remains in $\mathsf{P}$, even with $O(\log n)$
extra clauses.

######  Theorem 7.3.

MAJORITY-SAT over $2$-CNFs with $O(\log n)$ additional arbitrary width-clauses
is decidable in polynomial time.

###### Proof.

Let $F$ be a given $2$-CNF conjoined with $O(\log n)$ arbitrary-width clauses,
and let $\rho\in(0,1)$ be given. We wish to determine if
$\\#\text{SAT}(F)\geq\rho\cdot 2^{n}$. First, we imagine executing the
algorithm of Theorem 3.1 on just the $2$-CNF part of $F$, ignoring the
arbitary-width clauses for now. The algorithm either reports NO (in which case
we should also report NO) or it reports the exact number of SAT assignments to
the $2$-CNF part. In the latter case, the algorithm computes this number by
enumerating over all assignments to an $O(1)$-size set of variables, and
solving $\\#$SAT on $1$-CNFs obtained by each assignment. We can think of this
algorithm as in fact converting the given $2$-CNF into a decision tree of
depth $O(1)$, whose leaves are labeled by $1$-CNF formulas.

To solve $\\#$SAT for the entire instance (including the $O(\log n)$ long
clauses), we apply the Inclusion-Exclusion Principle. A well-known algorithm
for solving $\\#$CNF-SAT on $m$ clauses [FK10] works by repeatedly applying
the equation

$\displaystyle\\#\text{SAT}(F\wedge
C)=\\#\text{SAT}(F)-\\#\text{SAT}(F\wedge\neg C)$ (17)

to the clauses $C$ of a given formula. Letting $F^{\prime}$ be the $2$-CNF