Quelle est la complexité de Median-SAT?

Soit une formule CNF avec n variables et m clauses. Soit t ∈ { 0 , 1 } n une affectation de variable et f φ ( t ) ∈ { 0 , … , m } compte le nombre de clauses satisfaites par une affectation de variable à φ . Définissez ensuite Median-SAT comme le problème du calcul de la valeur médiane de f φ ( t ) sur tout t } n . Par exemple, si $\varphi$$n$$m$$t \in \{ 0,1 \}^n$$f_{\varphi}(t) \in \{ 0, \ldots , m \}$$\varphi$$f_{\varphi}(t)$$t \in \{ 0,1 \}^n$$\varphi$est une tautologie alors la solution à Median-SAT sera car indépendamment de l'affectation chaque clause sera satisfaite. Cependant, dans le cas de ¯ S A T, la solution de Median-SAT pourrait être comprise entre 0 et$m$$\overline{SAT}$$0$ .$m-1$

Cette question s'est posée lorsque je réfléchissais à deux extensions naturelles de SAT, MAX-SAT et #SAT, et quelle serait la difficulté du problème résultant si elles étaient réunies. Pour MAX-SAT, nous devons trouver une affectation de variable particulière pour maximiser le nombre de variables satisfaites par . Pour #SAT, nous devons compter le nombre d'affectations qui satisfont tous les $\varphi$$m$ clauses de . Cette variante se termine principalement comme une extension de #SAT (et en fait de #WSAT ), mais conserve une partie de la saveur de MAX-SAT en ce que nous comptons le nombre de clauses satisfaites plutôt que de simplement décider si elles sont toutes satisfaites ou ne pas.$\varphi$

Ce problème semble plus difficile que #SAT ou #WSAT. Pour chaque affectation de variable, #SAT décide du problème booléen de savoir si cette affectation satisfait ou non, alors que Median-SAT détermine "dans quelle mesure" φ est satisfait en termes de nombre de clauses auxquelles une affectation satisfait.$\varphi$$\varphi$

Je me rends compte que ce problème est quelque peu arbitraire; le calcul du nombre moyen ou mode de clauses satisfaites par chaque affectation de variable semble capturer la même qualité. De nombreux autres problèmes le sont probablement aussi.

Ce problème a-t-il été étudié, peut-être sous un autre aspect? Est-ce difficile par rapport à #SAT? Il n'est pas clair pour moi a priori que Median-SAT soit même contenu dans FPSPACE, bien qu'il semble être contenu dans FEXPTIME.

Étant donné une instance de SAT, un entier et une affectation de variable, nous pouvons décider en temps polynomial si exactement k clauses sont satisfaites, simplement en comptant le nombre de clauses qui sont satisfaites et en testant si ce nombre est égal à k . Par conséquent, nous pouvons calculer le nombre total d'assignations de variables satisfaisant exactement k clauses en utilisant un oracle #P .$k$$k$$k$$k$

Ainsi, comme Max-SAT, Median-SAT peut être calculé en temps polynomial en utilisant un oracle Cela montre que le problème est en F P # P ⊆ F P S P A C E .$\#P$$FP^{\#P} \subseteq FPSPACE$

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.