<p>The following paper answers the question in the affirmative – the variant remains NP-hard using a reduction from Monotone Planar 3-SAT:
<a href="http://epubs.siam.org/doi/abs/10.1137/1.9781611976465.105" rel="noreferrer">http://epubs.siam.org/doi/abs/10.1137/1.9781611976465.105</a>
(arXiv: <a href="http://arxiv.org/abs/2009.12369" rel="noreferrer">http://arxiv.org/abs/2009.12369</a>)</p>
<p>The paper presents a slightly more restricted variant, <strong>Monotone Planar 3-SAT with Neighboring Variable Pairs</strong>, 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.</p>

CC BY-SA 4.0
2021-01-31T23:20:31.730Z
2021-01-31T23:20:31.730Z
squire
<p>Below I show that reordering is not possible in any sense, so a new hardness proof from scratch is needed.</p>

<p>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.</p>

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

CC BY-SA 4.0
2019-10-28T05:45:39.197Z
2019-10-28T05:45:39.197Z
domotorp
<p>Background:</p>
<p>An instance of 3-SAT is called <strong>monotone</strong> if each clause consists only of positive literals or only of negative literals.</p>
<p>Given an instance <span class="math-container">$\phi$</span> of 3-SAT, we consider the bipartite graph <span class="math-container">$G_\phi$</span> 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 <span class="math-container">$G_\phi$</span> is planar then <span class="math-container">$\phi$</span> is also said to be <strong>planar</strong>.</p>
<p><strong>Planar Monotone 3-SAT</strong> (de Berg and Khosravi [<a href="https://www.win.tue.nl/%7Emdberg/Papers/2010/bk-obspp-10.pdf" rel="nofollow noreferrer">1</a>]) is an NP-hard SAT variant where instances are both monotone and planar.
Furthermore, it remains hard when the graph <span class="math-container">$G_\phi$</span> 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:</p>
<p><a href="https://i.sstatic.net/YHP4D.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/YHP4D.png" alt="enter image description here" /></a> <sup><i>(Figure adapted from [<a href="https://www.win.tue.nl/%7Emdberg/Papers/2010/bk-obspp-10.pdf" rel="nofollow noreferrer">1</a>]) </i></sup></p>
<p>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 <span class="math-container">$C$</span> if <span class="math-container">$C$</span> is horizontally between the two legs (and is on the same side as the legs with respect to the variables).</p>
<p>A new definition: A clause (of size 3) is <b>bi-enclosing</b> if both its leftmost and rightmost pair of legs enclose some other clauses. For example, in the figure above <span class="math-container">$C_i$</span> is the only bi-enclosing clause (as all others clauses have a pair of legs with no clauses between them).</p>
<p><strong>The SAT variant I'm asking about:</strong> All Planar Monotone 3-SAT instances in rectilinear representation where there are no bi-enclosing clauses. <em>Is deciding satisfiability in this case NP-hard?</em></p>
<p>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 [<a href="https://epubs.siam.org/doi/pdf/10.1137/0405033" rel="nofollow noreferrer">3</a>], has no bi-enclosing clauses:</p>
<p><a href="https://i.sstatic.net/5RNm8.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/5RNm8.png" alt="enter image description here" /></a></p>
<p><strong>Edit following domotorp's answer:</strong> Here is an instance where we cannot change the order of the variables in order to prevent <span class="math-container">$(x_1 ∨ x_3 ∨ x_5)$</span> from being bi-enclosing:</p>
<p><a href="https://i.sstatic.net/AAdJ1.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/AAdJ1.png" alt="enter image description here" /></a></p>
<p>(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 &quot;non-fixable&quot; instance in that case).</p>

<np-hardness><sat><planar-graphs><graph-drawing>
NP-hardness of a planar SAT variant
squire
# NP-hardness of a planar SAT variant

(Asked by: username_0 on 2019-10-27)

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](https://www.win.tue.nl/%7Emdberg/Papers/2010/bk-obspp-10.pdf)]) 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:

[![enter image description here](https://i.sstatic.net/YHP4D.png)](https://i.sstatic.net/YHP4D.png) *(Figure adapted from [[1](https://www.win.tue.nl/%7Emdberg/Papers/2010/bk-obspp-10.pdf)])*

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](https://epubs.siam.org/doi/pdf/10.1137/0405033)], has no bi-enclosing clauses:

[![enter image description here](https://i.sstatic.net/5RNm8.png)](https://i.sstatic.net/5RNm8.png)

**Edit following username_1'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:

[![enter image description here](https://i.sstatic.net/AAdJ1.png)](https://i.sstatic.net/AAdJ1.png)

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

**Tags:** np-hardness, sat, planar-graphs, graph-drawing


---

## 2 answers

### Answer by username_0 on 2021-01-31. Score: 5 | Accepted answer

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 by username_1 on 2019-10-28. Score: 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$.


---

