Is every X3SAT instance with no cycles satisfiable? Exactly 1 in 3 SAT (X3SAT) is a variation of the Boolean Satisfiability problem. Given a set of clauses, where each clause has three literals, is there an assignment such that in each clause exactly one literal is true?  X3SAT is NP-hard even if we assume all literals are positive (monotone) and no two clauses have more than one literal in common (linear).

A cycle is a set of clauses such that each clause has one free literal and two backbone literals. A literal is free if it appears in only one clause in the cycle. A backbone literal appears in exactly two cycle clauses.

My question: Is a linear and monotone X3SAT instance with no cycles always satisfiable?



Background: We can think of linear monotone X3SAT as the following problem:  we are given a set of clauses, where each clause has three positive literals and no two clauses have more than one literal in common; the goal is to determine whether there is a set of literals such that each clause contains exactly one literal from the set.

I have generated a number of unsatisfiable linear monotone X3SAT instances and they all have large numbers of cycles, so I'm wondering if every unsatisfiable linear monotone X3SAT instance will have at least one cycle.

The smallest linear and monotone cycle has three clauses:

$\quad$ 3-cycle: $(a,x_1,x_2)(b,x_2,x_3)(c,x_3,x_1)$
$\quad$ Free: $a,b,c$
$\quad$ Backbone: $x_1,x_2,x_3$  

A cycle can have more than three clauses.  A cycle with $k$ clauses has $2k$ distinct literals, $k$ free literals, and $k$ backbone literals. A $k$-cycle has $\lceil F_{k+3} / 2\rceil$ satisfying assignments, where $F_i$ is the $i$-th Fibonacci number.

The smallest unsatisfiable linear and monotone X3SAT instance has six 3-cycles, but only five clauses:

$\quad (a,x_1,y_1)(a,x_2,y_2)(a,x_3,y_3)(x_1,x_2,x_3)(y_1,y_2,y_3)$

It contains the following 3-cycles:

$\quad(x_1,x_2,x_3)(a,x_1,y_1)(a,x_2,y_2)$
$\quad(x_1,x_2,x_3)(a,x_1,y_1)(a,x_3,y_3)$
$\quad(x_1,x_2,x_3)(a,x_2,y_2)(a,x_3,y_3)$
$\quad(y_1,y_2,y_3)(a,x_1,y_1)(a,x_2,y_2)$
$\quad(y_1,y_2,y_3)(a,x_1,y_1)(a,x_3,y_3)$
$\quad(y_1,y_2,y_3)(a,x_2,y_2)(a,x_3,y_3)$  

X3SAT can be converted into a max weight independent set problem. Let each literal be assigned a vertex. Two vertices have an edge iff the two literals appear together in a clause. The weight of each vertex is the number of clauses the literal appears in (one half the degree of the vertex). The X3SAT instance is solvable only if there is an independent set with weight equal to the number of clauses. If the instance is satisfiable then the graph can be made bipartite by removing exactly one edge from each clause.
The graph below is a positive answer without words.


Here is the detailed proof.
Definitions
Let $X$ be an instance of X3SAT.

$X$ is linear if any two clause shares at most one variable.
$X$ is monotone if all literals in all clauses are positive.
A walk in $X$ is a sequence of clauses where each clause is not disjoint with the clause following it. The length of the walk is the number of its clauses. A walk starts with variable $v$ if its first clause contains $v$. A walk ends with variable $v$ if its last clause contains $v$. A walk is said to connect two variables if it starts with one of the variables and ends with the other variable. In particular, any clause connects all variables in it.
A trail is a walk in which all clauses are distinct.
$X$ is connected if there is a walk between any two variables.
A cycle is a walk whose first clause is its last clause. A simple cycle has no repeated clauses except the first and last clause. $X$ is acyclic if $X$ has no simple cycles, i.e., there is at most one trail between any two variables,
For any two variables, the distance between them is the minimum length of a walk that connects them. The distance between a variable and itself is 0.

A linear monotone acyclic instance of X3SAT is always satisfiable.
Let $X$ be a linear monotone acyclic instance of X3SAT whose set of variables is $V=\{v_1,v_2, \cdots, v_n\}$. Because of monotonicity, we will use variable and literal interchangeably. Each clause in $X$ is also treated as the set of three variables in it.
Assume $X$ is connected. Otherwise, $X$ is the union of two disjoint linear monotone acyclic instances of X3SAT that can be treated independently.
Let $d(u)$ denote the distance from $v_1$ to variable $u$.
Claim 1. For any clause $c=(t,u, w)$, $\{d(t), d(u), d(w)\}=\{\ell, \ell, \ell-1\}$ for some $\ell\ge1$.
Proof: If $c$ contains $v_1$, then it is easy to see that $\{d(t), d(u), d(w)\}=\{1, 1, 0\}$. Now assume $c$ does not contain $v_1$.
WLOG, let $d(w)=\ell-1 &gt; 0$ be the minimum among the three distances. Let $c_1, \cdots, c_{\ell-2}, c_{\ell-1}$ be the unique trail from $v_1$ to $w$. The shared variable between $c_{\ell-2}$ and $c_{\ell-1}$ cannot be $t$ or $u$, since $d(t)\ge \ell-1$ and $d(u)\ge\ell-1.$ That means $c_{\ell-1}\not=c$. Suppose there is a trail $b_1, b_2, \cdots, b_{\ell-1}$ from $v_1$ to $t$. Then for the same reason, $b_{\ell-1}\not=c$. We can reduce the walk $c_1, \cdots, c_{\ell-2}, c_{\ell-1}, c, b_{\ell-1}, b_{\ell-2}, \cdots, b_1, c_1$ to a simple cycle, which is a contradiction, which implies that there is no trails of length $\ell-1$ from $v_1$ to $t$, i.e., $d(t)\gt\ell-1$. Since $c_1, c_2, \cdots, c_{\ell-1}, c$ is a walk of length $\ell$ from $v_1$ to $t$,  $d(t)=\ell$. Similarly, $d(u)=\ell.$ QED.
Fix a total order $\prec$ on $V$. For example, we can let $v_p\prec v_q $ if $p&lt;q$.
Let $A_0=\{v_0\}$. For all $\ell\ge 1$, define $A_{\ell}$ recursively by
$$A_\ell=
\{t\in V: d(t)=\ell \text{ and the last clause of the shortest trail}\\
\text{ from } v_1\text{ to }t\text{ is }(t,u, w)\text{ for some }u,w\in V \text{ such that }\\
d(t)=d(u)=\ell\text{ and }d(w)=\ell-1\text{ and } w\not\in A_{\ell-1}\text{ and }t\prec u\}$$
Let $A=\cup_{\ell=0}^{\infty}A_\ell$. Note that if $d(t)=\ell$, then $t\in A$ iff $t\in A_\ell$.
Claim 2: $A$ shares exactly one variable with each clause.
Proof. Let $c$ be a clause in $X$. By claim 1, $c=(t,u,w)$ where $d(t)=d(u)=\ell$, $d(w)=\ell-1$ and $t\prec u$. The last clause of the shortest trail from $v_1$ to either $t$ or $u$ is $c$.

$w\in A_{\ell-1}$. By definition, $t$ and $u$ are not in $A_\ell$.
$w\not\in A_{\ell-1}$. By definition, $t\in A_\ell$ and $u\not\in A_\ell$.

QED.

Exercises
Let X be a linear monotone acyclic instance of X3SAT with $n$ variables and $m$ clauses.
Exercise 1..(One minute or two) Explain that $A_1$ is empty. Give an example where $A_3$ is not empty.
Exercise 2.. Show that $n= 2m+1$.