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

A cycle is a set of clauses so that each clause has a free literal and two backbone literals. A literal is free if it appears in a single clause in the cycle. A literal trunk network appears exactly in two cycle clauses. The smallest linear and monotonous cycle has three clauses. A cycle with $ k $ clauses has $ 2k $ different literals, $ k $ free literals, and $ k $ literals of the spine. A $ k-cycle $ have $ Roof (Fibonacci (k + 3) / 2) $ satisfactory tasks. The smallest unsatisfiable linear and monotonous 3SAT instance has six $ 3 cycles $, but only five clauses.

The smallest unsatisfiable instance:

(a, x1, y1) (a, x2, y2) (a, x3, y3) (x1, x2, x3) (y1, y2, y3)

3 cycles:

(x1, x2, x3) (a, x1, y1) (a, x2, y2)

(x1, x2, x3) (a, x1, y1) (a, x3, y3)

(x1, x2, x3) (a, x2, y2) (a, x3, y3)

(y1, y2, y3) (a, x1, y1) (a, x2, y2)

(y1, y2, y3) (a, x1, y1) (a, x3, y3)

(y1, y2, y3) (a, x2, y2) (a, x3, y3)

X3SAT can become a problem of independent set of maximum weight. Let each literal be assigned a vertex. Two vertices have an edge if the two literals appear together in a clause. The weight of each vertex is the number of clauses in which the literal appears (half of the degree of the vertex). The X3SAT instance can only be solved if there is an independent set with a weight equal to the number of clauses. If the instance is successful, then the graph can be made bipartite by removing exactly one edge of each clause.

Is a linear and monotone instance of X3SAT without cycles always satisfactory?