Is every X3SAT instance with no cycles satisfiable?

Question

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.

Answer 1

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

Answer 2

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:

$\quad(a,b,z)(a,c,e)(c,f,g)(f,h,i)(b,x,y)(z,j,k)$

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

$\quad(b,x,y)(z,j,k)(c,f,g)$.

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)(b,d,e)(c,f,g)(d,f,h)$

$\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)$

$\quad(A,b,c)(b,D,e)(c,f,G)(D,f,h)$

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.

---

I want to correct this answer. This proof shows a linear, monotone X3SAT instance is solvable unless there exists a clause where all three literals in the clause are backbone literals. This is not the same as saying the instance has no intersecting clauses as I mistakenly claimed. In some ways, this is a stronger claim since an instance can have intersecting cycles and still have no clause where all three literals are backbone literals.

This is an example of an instance that has no intersecting cycles, yet, there is a clause with three backbone literals:

$\quad(a1, x1, x2) (a2, x2, x3) (a3, x3, x1)$

$\quad(b1, y1, y2) (b2, y2, y3) (b3, y3, y1)$

$\quad(c1, z1, z2) (c2, z2, z3) (c3, z3, z1)$

$\quad(x1, y1, z1)$

x1, y1, and z1 are backbone literals even though the clause (x1, y1, z1) is not part of any cycle.

The algorithm does find satisfying assignments for this instance. Choosing a1 to be the origin gives the solution where a1, a3, y1, a2, c1, c3, b2, and c2 are true and all other variables are false.

$\quad(A1, x1, x2)(A2, x2, x3)(A3, x3, x1)$

$\quad(b1, Y1, y2)(B2, y2, y3)(b3, y3, Y1)$

$\quad(C1, z1, z2)(C2, z2, z3)(C3, z3, z1)$

$\quad(x1, Y1, z1)$