NP-hardness of a planar SAT variant

Question

Background:

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 [1]) 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 [1])}

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 [3], 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).

Answer 1

The following paper answers the question in the affirmative – the variant remains NP-hard using a reduction from Monotone Planar 3-SAT: http://epubs.siam.org/doi/abs/10.1137/1.9781611976465.105 (arXiv: http://arxiv.org/abs/2009.12369)

The paper presents a slightly more restricted variant, Monotone Planar 3-SAT with Neighboring Variable Pairs, which requires each clause with three variables to contain two variables that are adjacent on the line on which all variables are embedded. If there is a bi-enclosing clause in this variant, it must enclose a redundant clause due to monotonicity, so we can assume no bi-enclosing clauses.

Answer 2

Below I show that reordering is not possible in any sense, so a new hardness proof from scratch is needed.

It's not even possible to reorder just one side if you don't eliminate redundant cluases. This is because any pair of adjacent (cyclically) variables can be in a clause and that gives you very little freedom, you can only reorder them by a cyclical shift.

The same issue comes up when there are no (trivially) redundant cluases. If a cluase $C_0$ has degree 3, and it bi-encloses $C_1$ and $C_2$, while $C_0$ is also enclosed by $C_3$, then in any reordering $C_0$ will still bi-enclose two of $C_1$, $C_2$ and $C_3$.