MSAT and IMSAT problems (restricted versions of SAT)

Question

I was reading about about NP-intermediate problems on Wikipedia and saw the IMSAT problem mentioned over there.

There is no Wikipedia page for that problem and they only cite this paper.

In the paper they define the MSAT problem as:

Recall that the satisfiability problem (SAT) is to decide whether a set of propositional clauses $C = \{C_1, ... ,C_m\}$, where each $C_i$ is a set of literals, on atoms $X = \{x_1, ... , x_n \}$ is satisfied by some truth assignment to $X$. Its restriction $MSAT$, where every clause of $C$ must be either positive or negative, i.e., must not contain any negative or positive literal, respectively, is still NP-hard.

But they don't reference any source that prove $MSAT$ is indeed NP-Hard. Can you please enlighten me?

Moreover, they later introduce the problem of IMSAT by:

The first subcase of MSAT which we consider is made up of instances with the property that every pair of a positive clause and a negative clause resolves, i.e. there is an atoms which occurs unnegated in the positive and negated in the negative clause.

I don't understand why Wikipedia mentioned this problem as NP-intermediate, this term was never shown in the paper. I see they prove that co-IMSAT is TRANS-HYP-complete, but couldn'tunderstand if TRANS-HYP is NP-intermediate, and what does it say on IMSAT.

I got a mess here, and I couldn't find any other sources. Is MSAT NP-Hard? I would like to see a proof (or at least an idea for a proof) Is IMSAT NP-intermediate? A proof of that seems to be missing as well, or I totally didn't understand the paper.

And another a bit more general question about using NP-intermediate problems:

If I understand correctly, it is quiet impossible to prove something is in NP-intermediate, since the class is defined as problems that polynomial running time solution was not found for them, and they were not proven to be NP-Hard (though they are in NP). If I want to "lean" on IMSAT as NP-intermediate. how can I do that?

Lets say I have a reduction from IMSAT to my problem P, which means if P is solvable in polynomial time, IMSAT as well. What paper can I cite to show that IMSAT in NP-intermediate - which can convince people P is a hard problem (and it is fair to use approximate/probabilistic algorithm instead of trying to solve it)

Answer 1

For your first question, I'll give an elementary proof for the $\mathsf{NP}$-hardness of $\mathrm{MSAT}$ by reduction from $\mathrm{SAT}$.

Let $\varphi$ be a propositional formula in CNF (i.e., a $\mathrm{SAT}$ instance) consisting of the clauses $C_1, ..., C_m$ and let $C_i^+$ and $C_i^-$ denote the set of positive and negative literals of the clause $C_i$, respectively.

I illustrate the idea using an example: Suppose we have a clause $C = (x_1 \vee x_2 \vee \neg x_3)$. The idea will be to introduce a new literal $c$ to split $C$ into $C^+ \cup \{c\}$ and $C^- \cup \{\neg c\}$ to obtain two new clauses which are either positive or negative. In this example, we get $(x_1 \vee x_2 \vee c) \wedge (\neg c \vee \neg x_3)$, and it is not hard to see that this formula is indeed equivalent to $C$ itself: Any satisfying assignment of $C$ must satisfy at least one of our two new clauses, and by choosing the assignment to $c$ accordingly, we can satisfy both. Conversely, any assignment to $c$ can only satisfy one of the clauses and hence, a satisfying assignment to both clauses must, if restricted to the variables $x_1, x_2$ and $x_3$, satisfy $C$.

By applying this construction to all clauses, we obtain a formula $\varphi'$ which is equivalent to $\varphi$ but only contains positive and negative clauses. Clearly, $\varphi'$ can be computed from $\varphi$ in polynomial time, and we conclude that $\mathrm{MSAT}$ is $\mathsf{NP}$-hard.

On the second question (and the ones following): We do not know any $\mathsf{NP}$-intermediate problems (that is why the section title in the linked Wiki article contains "might"). By Ladner's theorem, such problems exist if and only if $\mathsf P \neq \mathsf{NP}$, which is an open question. Hence, you probably won't find papers showing (unconditionally) that $\mathrm{IMSAT}$ is $\mathsf{NP}$-intermediate.

One can speculate that problems which have evaded the $\mathsf P$/$\mathsf{NP}$-completeness classification for a long time could be intermediate, but speculation it is. In some cases, like the Graph Isomorphism problem, better arguments than "it hasn't been resolved either way for a long time" can be made: Under common complexity-theoretic assumptions (specifically, a non-collapse of the polynomial hierarchy), graph isomorphism is not $\mathsf{NP}$-hard. On the other hand, much research has been invested into finding polynomial-time algorithms for GI, yielding to many such algorithms for special cases and a general quasi-polynomial-time algorithm recently developed by László Babai.

I am not aware of similar "evidence" for $\mathrm{IMSAT}$, though it is not my field of expertise -- maybe someone else can expand on that.