I have extended this proof to show a linear, monotone X3SAT instance with any number of non-intersecting cycles is always satisfiable. Two cycles intersect if they have a variable in common
Cases to consider include cycles with an even number of clauses, cycles with an odd number of clauses, a cycle that contains the origin, and cycles that don't contain the origin. Since the algorithm described sometimes chooses literals lexicographically, the way a cycle is labeled can change the satisfying assignment found. The following algorithm handles all of these cases. The basic idea is to totally order the clauses and then satisfy each clause in order while doing the X3SAT equivalent of unit clause propagation.
Assume every literal can be lexicographically ordered. Create a graph by assigning a vertex to each literal. Two literals are connected by an edge if the two literals appear together in a clause. The X3SAT instance is satisfiable if the graph can be made bipartite by removing one edge from each clause.
Choose the lexicographically lowest order literal and make it the origin of the graph. Assume this literal is assigned true. The distance between a literal and the origin is the smallest number of edges connecting the literal to the origin. The distance of a clause from the origin is the distance from the origin to the closest literal(s) in the clause.
At this point I want to define several types of literals. A cycle has two types of literals: "Backbone" literals are literals that appear in two of the cycle's clauses. "Free" literals appear in only one of the cycle's clauses.
Apass Jack proves every clause has one literal that is "closest" to the origin and two "furthest" literals in a linear, monotone X3SAT instance with no cycles. In a linear, monotone X3SAT instance with no intersecting cycles it is possible for a clause to have two closest literals, but, no clause can have all three literals the same distance from the origin. For a clause to have two closest literals, both literals must be backbone literals in a cycle. If all three literals in the clause are the same distance from the origin then all three literals must be backbone literals in a cycle. This would require the clause to be in three intersecting cycles and we are assuming the instance has no intersecting cycles. This shows every clause must have at least one literal "closest" to the origin and at least one "furthest" literal.
Order the clauses by their distance from the origin. We will "impose" an order on furthest literals based on the order of the clauses that are the same distance from the origin.
Clauses that are the same distance from the origin should first be ordered by the imposed order of their closest literals and then ordered by the lexicographically lowest ordered furthest literal. This determines a total order of the clauses and imposes a total order on the literals. Here is an example:
$a$ is the origin.
$\quad(a,b,z)$ and $\quad(a,c,e)$ are distance-$0$ from the origin.
We order them first by the closest literal which is $a$ in both clauses. Then we order them by the lexicographically lowest ordered furthest literal. $b$ comes before $c$, so,
$\quad(a,b,z)$ comes before $\quad(a,c,e)$.
This imposes the order $a,b,z,c,e$ on the literals in distance-$0$ clauses. The clauses
$\quad(c,f,g), (b,x,y), (z,j,k)$
are distance-$1$ from the origin. We first order these clauses by the closest literals using the imposed order:
This is enough to order the clauses and imposes the order $a,b,z,c,e,x,y,j,k,f,g$.
$\quad(f,h,i)$ is the only distance-$2$ clause from the origin.
Clausal order: $\quad(a,b,z)(a,c,e)(b,x,y)(z,j,k)(c,f,g)(f,h,i)$
Imposed literal order: $a,b,z,c,e,x,y,j,k,f,g,h,i$
Process each clause in order. Note that as each clause is processed the literal(s) closest to the origin already have an assignment from a previous step. For example, in distance-$0$ clauses, the origin has already been assigned to true. This means all other literals in distance-$0$ clauses must be false. The closest literal in distance-$1$ clauses must be one of those literals assigned false in distance-$0$ clauses. Similarly, the closest literal(s) in each clause will have been assigned a truth value in an earlier step.
When a clause is processed in order, all of the assigned literal(s) will be false, Choose the lowest order unassigned literal in the clause and assign it true. All other literals in the clause are assigned false. Propagate these assignments to other clauses. In particular, when an unassigned literal is assigned to true then process all clauses with this literal immediately and set all other literals in these clauses to false (unit clause propagation).
An example. The instance is listed in clausal order.
4-Cycle that contains the origin:
$\quad(a,b,c)$ : $A$ is the origin and assigned true so $b$ and $c$ must be false: $\quad(A,b,c)$
$\quad(b,d,e)$ : $b$ is false so choose the lowest order unassigned furthest literal, $D$, to be true: $\quad(b,D,e)$
$\quad(d,f,h)$ : Propagate $D$ is true and set $f$ and $h$ to false: $\quad(D,f,h)$
$\quad(c,f,g)$ : $c$ and $f$ are false so the lowest order unassigned furthest literal, $G$, is set true: $\quad(c,f,G)$
Proof of the correctness of the algorithm.
Every clause will be either processed in order or processed out of order.
A clause is processed out of order when a previous step sets a literal in the clause to true (unit propagation step). All other literals in the clause are set to false and the clause will always be satisfied if it is processed out of order.
When a clause is processed in order then all of the closest literals will have been set to false in a previous step. If the clause is part of a cycle then it is possible one of the furthest literals may have been set to false in a previous step. This can only happen if the furthest literal is a backbone literal. This happens in the example above. When $\quad(b,D,e)$ is processed, $D$ is set to true and this propagates to $\quad(D,f,h)$ forcing $f$ to be false. $f$ is a backbone literal in the $4$-cycle and a furthest literal in $\quad(c,f,g)$. I have already shown that all three literals in a clause can't be backbone literals because this would require intersecting cycles. This means when a clause is processed in order there must be at least one unassigned furthest literal in the clause. This literal can be set to true satisfying the clause (this is literal $G$ in $\quad(c,f,G)$ in the example).
This proves the algorithm will satisfy all clauses in a linear, monotone X3SAT instance with no intersecting cycles.