<p>The considered instances have bounded (primal) pathwidth, hence bounded primal treewidth too and can hence be solved in linear time. This result is actually hard to trace in the literature as it has been observed independently in various formalism. [1] is the reference where you can find the most straightforward statement of the result. And [3] contains a more self contained approach algorithms with generalisations to #SAT and other measures. To the best of my knowledge, [2conf, 2] is the first reference where tractability for primal treewidth has been proven but it is formulated as branch width which is an equivalent measure, and [1] does the link between two notions. [2] uses  Davis Putnam resolution on a well chosen order that terminates in polynomial time when primal tree width is bounded. [4] is the first reference where such a result have been stated and proven for treewidth explicitly.</p>
<p>You can observe that the more general instances where for every clause, its variables are included in <span class="math-container">$\{x_{i-k}, \dots, x_{i+k}\}$</span> for some <span class="math-container">$i$</span> have pathwidth at most <span class="math-container">$4k+1$</span>, and hence can also be solved in polynomial time (with an exponential dependency on <span class="math-container">$k$</span>).</p>
<p>To see this, define <span class="math-container">$A_i = \{x_{(i-k)\ mod\ n}, \dots, x_{(i+k)\ mod\ n}\}$</span>  and <span class="math-container">$B_i = A_1 \cup A_i$</span>. Consider the path decomposition <span class="math-container">$B_1, \dots, B_{n}$</span>. Every clause is included in at least one bag <span class="math-container">$B_i$</span> by definition. Every bag has size <span class="math-container">$4k+2$</span> and hence the width of the decomposition is bounded by <span class="math-container">$4k+1$</span>. Finally, every variable is connected in the decomposition. This is obvious for variables in <span class="math-container">$A_1$</span> since <span class="math-container">$A_1 \subseteq B_i$</span> for every <span class="math-container">$i$</span>. For other variables, observe that <span class="math-container">$x_i$</span> for <span class="math-container">$k&lt;i&lt;n-k$</span>  (that is <span class="math-container">$x_i \notin A_1$</span>) appears exactly in <span class="math-container">$B_{i-k}, \dots, B_{i+k}$</span>, which are connected in the path decomposition.</p>
<h1>References</h1>
<p>[1] Stefan Szeider, On fixed-parameter tractable parameterizations of SAT.
In E. Giunchiglia and A. Tacchella, editors, Theory and Applications of Satisfiability, 6th International Conference, volume 2919 of LNCS, pages 188–202. Springer, 2004. 85, 103</p>
<p>[2conf] M. Alekhnovich and A. A. Razborov. Satisfiability, branch-width and Tseitin
tautologies. In 43rd Annual IEEE Symposium on Foundations of Computer Science
(FOCS’02), pages 593–603, 2002.</p>
<p>[2] M. Alekhnovich and A. Razborov. Satisfiability, Branch-Width and Tseitin tautologies. Computational Complexity, 20(4):649–678, November 2011. 103</p>
<p>[3] Samer, M., &amp; Szeider, S. (2010). Algorithms for propositional model counting. Journal of Discrete Algorithms, 8(1), 50-64.</p>
<p>[4] G. Gottlob, F. Scarcello, and M. Sideri. Fixed-parameter complexity in AI and nonmonotonic reasoning. Artificial Intelligence, 138(1-2):55–86, 2002.</p>

CC BY-SA 4.0
2024-10-08T22:31:54.087Z
2024-10-09T14:20:38.397Z
2024-10-09T14:20:38.397Z
holf
<p>In 3-Sat problem, the input is a set <span class="math-container">$X$</span> of variables and a set <span class="math-container">$C$</span> of clauses, each containing 3 literals over <span class="math-container">$X$</span>. This problem is NP-complete even if the variable-clause incidence graph of the formula is guaranteed to be planar (called Planar 3-Sat).
How about we fix a cyclic ordering of the variables (e.g. <span class="math-container">$x_1,x_2,\dots,x_n$</span>) and demand that each clause contains 3 consecutive variables? (that is, each clause is a 3-element subset of <span class="math-container">$\{x_{i-1},\bar{x}_{i-1},x_i,\bar{x}_i,x_{i+1},\bar{x}_{i+1}\}$</span> where the indices are modulo <span class="math-container">$n$</span>). Let us call this problem Path Convex 3-Sat.
I think Path Convex 3-Sat is polynomial-time solvable. Can we prove that the following slightly relaxed version is NP-complete?</p>
<ul>
<li>Each clause is a 3-element subset of <span class="math-container">$\{x_{i-1},\bar{x}_{i-1},x_i,\bar{x}_i,x_{i+1},\bar{x}_{i+1},x_{i+2},\bar{x}_{i+2}\}$</span>, where the indices are modulo <span class="math-container">$n$</span>.</li>
</ul>
<p>Comment: I feel that this problem belong somewhere between Variable-Cycle Planar 3-Sat, and Variable-Cycle 1-Planar 3-Sat (see <a href="https://arxiv.org/pdf/1710.07476v6" rel="nofollow noreferrer">Pilz</a> for definition).</p>

CC BY-SA 4.0
2024-10-08T11:32:53.667Z
In both cases you have bounded pathwidth (3 in the first case, 4 in the second, if clause $x_{n-1} \vee x_n \vee x_1$ is allowed (if no cycle is allowed then pathwidth becomes respectively 2 and 3). So yes, you can solve it in linear time. Even Davis Putnam resolution following the cycle order should finish in polynomial time.
holf
CC BY-SA 4.0
2024-10-08T11:51:33.167Z
@holf Okay, please post it as an answer. I shall edit the question to clarify that the indices are modulo $n$.
Cyriac Antony
CC BY-SA 4.0
2024-10-08T15:24:39.537Z
@holf I would greatly appreciate if you can give the reference or hint. Is the reference *S. Szeider, On ﬁxed-parameter tractable parameterizations of SAT*?
Cyriac Antony
CC BY-SA 4.0
2024-10-08T22:08:52.677Z
Yes, this is the one, I write an full answer tomorrow.
holf
<cc.complexity-theory><np-hardness>
Complexity of Almost Path Convex 3-Sat
Cyriac Antony
# Complexity of Almost Path Convex 3-Sat

(Asked by: username_0 on 2024-10-08)

In 3-Sat problem, the input is a set $X$ of variables and a set $C$ of clauses, each containing 3 literals over $X$. This problem is NP-complete even if the variable-clause incidence graph of the formula is guaranteed to be planar (called Planar 3-Sat).
How about we fix a cyclic ordering of the variables (e.g. $x\_1,x\_2,\dots,x\_n$) and demand that each clause contains 3 consecutive variables? (that is, each clause is a 3-element subset of $\{x\_{i-1},\bar{x}\_{i-1},x\_i,\bar{x}\_i,x\_{i+1},\bar{x}\_{i+1}\}$ where the indices are modulo $n$). Let us call this problem Path Convex 3-Sat.
I think Path Convex 3-Sat is polynomial-time solvable. Can we prove that the following slightly relaxed version is NP-complete?

* Each clause is a 3-element subset of $\{x\_{i-1},\bar{x}\_{i-1},x\_i,\bar{x}\_i,x\_{i+1},\bar{x}\_{i+1},x\_{i+2},\bar{x}\_{i+2}\}$, where the indices are modulo $n$.

Comment: I feel that this problem belong somewhere between Variable-Cycle Planar 3-Sat, and Variable-Cycle 1-Planar 3-Sat (see [Pilz](https://arxiv.org/pdf/1710.07476v6) for definition).

**Tags:** cc.complexity-theory, np-hardness

> **Comments:**
> **username_1**: In both cases you have bounded pathwidth (3 in the first case, 4 in the second, if clause $x_{n-1} \vee x_n \vee x_1$ is allowed (if no cycle is allowed then pathwidth becomes respectively 2 and 3). So yes, you can solve it in linear time. Even Davis Putnam resolution following the cycle order should finish in polynomial time.  
> **username_0**: @username_1 Okay, please post it as an answer. I shall edit the question to clarify that the indices are modulo $n$.  
> **username_0**: @username_1 I would greatly appreciate if you can give the reference or hint. Is the reference *S. Szeider, On ﬁxed-parameter tractable parameterizations of SAT*?  
> **username_1**: Yes, this is the one, I write an full answer tomorrow.  

---

## 1 answers

### Answer by username_1 on 2024-10-08. Score: 2 | Accepted answer

The considered instances have bounded (primal) pathwidth, hence bounded primal treewidth too and can hence be solved in linear time. This result is actually hard to trace in the literature as it has been observed independently in various formalism. [1] is the reference where you can find the most straightforward statement of the result. And [3] contains a more self contained approach algorithms with generalisations to #SAT and other measures. To the best of my knowledge, [2conf, 2] is the first reference where tractability for primal treewidth has been proven but it is formulated as branch width which is an equivalent measure, and [1] does the link between two notions. [2] uses Davis Putnam resolution on a well chosen order that terminates in polynomial time when primal tree width is bounded. [4] is the first reference where such a result have been stated and proven for treewidth explicitly.

You can observe that the more general instances where for every clause, its variables are included in $\{x\_{i-k}, \dots, x\_{i+k}\}$ for some $i$ have pathwidth at most $4k+1$, and hence can also be solved in polynomial time (with an exponential dependency on $k$).

To see this, define $A\_i = \{x\_{(i-k)\ mod\ n}, \dots, x\_{(i+k)\ mod\ n}\}$ and $B\_i = A\_1 \cup A\_i$. Consider the path decomposition $B\_1, \dots, B\_{n}$. Every clause is included in at least one bag $B\_i$ by definition. Every bag has size $4k+2$ and hence the width of the decomposition is bounded by $4k+1$. Finally, every variable is connected in the decomposition. This is obvious for variables in $A\_1$ since $A\_1 \subseteq B\_i$ for every $i$. For other variables, observe that $x\_i$ for $k (that is $x\_i \notin A\_1$) appears exactly in $B\_{i-k}, \dots, B\_{i+k}$, which are connected in the path decomposition.

# References

[1] Stefan Szeider, On fixed-parameter tractable parameterizations of SAT.
In E. Giunchiglia and A. Tacchella, editors, Theory and Applications of Satisfiability, 6th International Conference, volume 2919 of LNCS, pages 188–202. Springer, 2004. 85, 103

[2conf] M. Alekhnovich and A. A. Razborov. Satisfiability, branch-width and Tseitin
tautologies. In 43rd Annual IEEE Symposium on Foundations of Computer Science
(FOCS’02), pages 593–603, 2002.

[2] M. Alekhnovich and A. Razborov. Satisfiability, Branch-Width and Tseitin tautologies. Computational Complexity, 20(4):649–678, November 2011. 103

[3] Samer, M., & Szeider, S. (2010). Algorithms for propositional model counting. Journal of Discrete Algorithms, 8(1), 50-64.

[4] G. Gottlob, F. Scarcello, and M. Sideri. Fixed-parameter complexity in AI and nonmonotonic reasoning. Artificial Intelligence, 138(1-2):55–86, 2002.


---

