An instance of 3-SAT is called monotone if each clause consists only of positive literals or only of negative literals.
Given an instance $\phi$ of 3-SAT, we consider the bipartite graph $G_\phi$ that contains a vertex per each variable and per each clause, and has an edge between a variable-vertex and a clause-vertex if and only if the variable appears in the clause. When $G_\phi$ is planar then $\phi$ is also said to be planar.
Planar Monotone 3-SAT (de Berg and Khosravi ) is an NP-hard SAT variant where instances are both monotone and planar. Furthermore, it remains hard when the graph $G_\phi$ has the following rectilinear representation: All variable-vertices lie on a horizontal line and all positive clause vertices are above it and all the negative clause vertices are below it. For example:
(Figure adapted from )
In this representation, each clause has at most 3 vertical lines, called legs, that go up/down to each of the variables it contains. We say that two legs enclose a clause $C$ if $C$ is horizontally between the two legs (and is on the same side as the legs with respect to the variables).
A new definition: A clause (of size 3) is bi-enclosing if both its leftmost and rightmost pair of legs enclose some other clauses. For example, in the figure above $C_i$ is the only bi-enclosing clause (as all others clauses have a pair of legs with no clauses between them).
The SAT variant I'm asking about: All Planar Monotone 3-SAT instances in rectilinear representation where there are no bi-enclosing clauses. Is deciding satisfiability in this case NP-hard?
I haven't seen this version addressed explicitly before. Interestingly, the first example of the rectilinear representation for (the more general) planar 3-SAT problem, given in Knuth and Raghunatan , has no bi-enclosing clauses:
Edit following domotorp's answer: Here is an instance where we cannot change the order of the variables in order to prevent $(x_1 ∨ x_3 ∨ x_5)$ from being bi-enclosing:
(Note that in the variant in question we cannot move clauses to the other side of the variables. In Planar 3-SAT, however, we could easily do that to fix the bad clause above and so a more complex example would be required for a "non-fixable" instance in that case).