What's the complexity of Median-SAT?

Question

Let $\varphi$ be a CNF formula with $n$ variables and $m$ clauses. Let $t \in \{ 0,1 \}^n$ represent a variable assignment and $f_{\varphi}(t) \in \{ 0, \ldots , m \}$ count the number of clauses satisfied by a variable assignment to $\varphi$. Then define Median-SAT as the problem of computing the median value of $f_{\varphi}(t)$ over all $t \in \{ 0,1 \}^n$. For example, if $\varphi$ is a tautology then the solution to Median-SAT will be $m$ since regardless of assignment every clause will be satisfied. However in the case of $\overline{SAT}$ the solution to Median-SAT could be anywhere between $0$ and $m-1$.

This question arose when I was pondering two natural extensions of SAT, MAX-SAT and #SAT, and what the difficulty of the resulting problem would be if they were put together. For MAX-SAT we have to find a particular variable assignment to maximize the number of variables satisfied by $\varphi$. For #SAT we have to count how many assignments satisfy all $m$ clauses of $\varphi$. This variant winds up mainly as an extension of #SAT (and in fact of #WSAT), but retains some of the flavor of MAX-SAT in that we count the number of satisfied clauses rather than just deciding whether they're all satisfied or not.

This problem seems harder than #SAT or #WSAT. For each variable assignment #SAT decides the Boolean problem of whether that assignment satisfies $\varphi$ or not whereas Median-SAT determines "to what extent" $\varphi$ is satisfied in terms of the number of clauses that an assignment satisfies.

I realize that this problem is somewhat arbitrary; computing the average or mode number of clauses satisfied by each variable assignment seems to capture the same quality. Probably many other problems do too.

Has this problem been studied, perhaps under a different guise? How hard is it compared to #SAT? It's not clear to me a priori that Median-SAT is even contained in FPSPACE, although it does seem to be contained in FEXPTIME.

Answer 1

Given an instance of SAT, an integer $k$, and a variable assignment, we can decide in polynomial time whether exactly $k$ clauses are satisfied, simply by counting the number of clauses that are satisfied and testing whether that number equals $k$. Hence we can calculate the total number of variable assigments satisfying exactly $k$ clauses using a #P oracle.

So like Max-SAT, Median-SAT can be computed in polynomial time using a $\#P$ oracle. This shows that the problem is in $FP^{\#P} \subseteq FPSPACE$.

Answer 2

This problem can be solved using $\lceil \lg m+1 \rceil$ invocations of an oracle for MAJSAT.

Let $M(\varphi)$ denote the desired median value for $\varphi$. For fixed $k$, define the formula $\psi_k$ so it is true for assignment $x$ iff $x$ satisfies at least $k$ of the clauses of $\varphi$. Notice that given $\varphi$ in CNF form and given $k$, you can easily construct $\psi_k$ in CNF form in polynomial time.

Now suppose we had an oracle for MAJSAT. Querying it on the formula $\psi_k$ would tell us whether the majority of assignments make the formula $\psi_k$ true, or equivalently, whether $M(\varphi) \ge k$. So, to learn $M(\varphi)$, apply binary search (start with $k=m/2$, then increase or decrease $k$ according to the results from the oracle). After $\lg m+1$ iterations, the binary search reveals the value of $M(\varphi)$. Each iteration requires one query to our oracle for MAJSAT.