# NP-hardness of a planar SAT variant

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

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