13
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ It's in $FP^{\#P}\subseteq FPSPACE$: for each $k\leq m$ we can count the number of assignments satisfying at least $k$ clauses using a #P oracle. $\endgroup$ – Colin McQuillan Feb 7 '11 at 11:31
  • 1
    $\begingroup$ @Colin make this into an answer ? $\endgroup$ – Suresh Venkat Feb 7 '11 at 19:29
  • $\begingroup$ Yes, this would make a good answer. Could you elaborate on how to query the #P oracle to check whether $k \leq m $ clauses are satisfied? I couldn't figure out how to do it efficiently. $\endgroup$ – Huck Bennett Feb 7 '11 at 19:37
  • $\begingroup$ @Tsuyoshi, what is your definition of SAT? Are we allowing repetition of clauses? or literals and/or variables in a given clauses? Because if you do not allow repetition of literals and/or variables in a given clauses you cannot have a CNF formula that is a tautology.. $\endgroup$ – Tayfun Pay Feb 11 '11 at 13:35
  • $\begingroup$ @Tayfun - I actually asked this question, Tsuyoshi helped with a minor edit. You're right about a tautology in a CNF formula requiring repeated literals. Any SAT variant would be interesting, CNF-SAT w/o var repetition in clauses (in which case tautologies are impossible), or maybe CIRCUIT-SAT more generally. I don't think this choice changes the flavor of the question. $\endgroup$ – Huck Bennett Feb 11 '11 at 15:23
12
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ You're absolutely right. This is a very clean argument, and I guess pretty obvious from the definition of #P. I learned something. $\endgroup$ – Huck Bennett Feb 17 '11 at 2:45
  • 1
    $\begingroup$ Let me elaborate on this a little more: Colin's saying that because we can determine in polynomial time whether a particular variable assignment satisfies $k$ clauses that we can nondeterministically guess a variable assignment and then count how many accepting paths (i.e. accepting variable assignments) this query had using the $\#P$ oracle (by definition of $\#P$). By iterating through k=1 to m, we can count the median number of clauses satisfied in $FP^{\#P}$. $\endgroup$ – Huck Bennett Feb 19 '11 at 5:25
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.