Limited number of variable occurrences in 1-in-3 SAT

Question

Is there a known result on complexity class of 1-in-3-SAT with restricted number of variable occurrences?

I've come up with the following parsimonious reduction with Peter Nightingale, but I want to cite something if this is known.

Here is the trick we came up with. This shows that 1-in-3-SAT limited to 3 occurrences per variable is NP complete and #P complete (since 1-in-3-SAT is), while 3-SAT limited to 3 occurrences is in P

Let’s say we have more than three occurrences of x. Say we need 6. Then we will introduce 5 new variables x2 to x6 equivalent to x and two new variables d1 and d2 guaranteed to be false with the following 6 new clauses:

x  -x2 d1
x2 -x3 d1
x3 -x4 d1
x4 -x5 d2
x5 -x6 d2
x6 -x  d2

Obviously we replace each occurrence of x after the first one by xi for some i. That gives three occurrences of each xi and d.

The above sets each di to false and all the xi to the same value. To see this, x has to be true or false. If it's true then the first clause sets x2 true and d1 false, and then this propagates down the clasues. If x is false then the last clause sets x6 false and d2 false and it propagates up the clauses. It's obviously strongly parsimonious so preserves counting.

Answer 1

Up to my knowledge the current "limits" have been settled in:

Stefan Porschen, Tatjana Schmidt, Ewald Speckenmeyer, Andreas Wotzlaw: XSAT and NAE-SAT of linear CNF classes. Discrete Applied Mathematics 167: 1-14 (2014)

See also Schmidt's Thesis: Computational Complexity of SAT, XSAT and NAE-SAT for linear and mixed Horn CNF formulas

Theorem 29. XSAT remains NP-complete for $k$-$CNF^l_+$ and $k$-$CNF^l$, $k, l \geq 3$.

(XSAT for $3$-$CNF^3$ is exactly 1-in-3-SAT where each variable appears exactly $l=3$ times)

Note that the theorem also proves the NP-completeness of the stronger monotone case ($CNF_+$)

Answer 2

(I understand this must be a late answer; i am writing for future readers)

There is an evern stronger result in the literature.

Cubic Planar Positive 1-in-3 Satisfiability is proved NP-complete in Moore and Robson, Hard Tiling Problems with Simple Tiles. (They say 'monotone' rather than 'positive'. See note added at last)

The mentioned result is stronger than the result in Schmidt's thesis because here the the graph of the formula is restricted to be planar. (The condition is in fact stronger: they give a particular kind of embedding called rectilinear embedding)

The graph $G_B$ of a boolean formula $B=(X,C)$ is defined as the the graph with vertex set $X\cup C$ and edge set $E:= \{ x_iC_j\ :\ $ variable $x_i$ occurs in clause $C_j$ (unnegated or negated) $\}$ (where $X$ is the set of variables and $C$ is the set of clauses).

Cubic Planar Positive 1-in-3 Satisfiability
Instance: A boolean formula $B=(X,C)$ where $X$ is a set of variables, $C$ a set of 3-element subsets over $X$ (clauses), and the graph $G_B$ of $B$ is a cubic planar graph.
Question: Does there exist a truth assignment for $X$ such that each clause is $C$ has exactly one true variable?

Note that each clause contains exactly 3 distinct variables and each variable appears in exactly 3 clauses.

See Tippenhauer's thesis On Planar 3-SAT and its Variants(2016) for sat variants that restrict number of variable occurrences.
Note: there are a few variants discovered after the publication of this thesis.

Note Added: The result of Moore and Robson proved that Cubic Planar Positive 1-in-3 Satisfiability is NP-complete. (That is, the boolean formula is not just monotone, it is Positive (ie, no negated literals at all) ). Unfortunately, in many early papers, the term 'monotone' was used to mean 'positive'. The reduction by Moore and Robson doesn't introduce negated literals. Their reduction is from Planar 'Monotone' 1-in-3 Satisfiability in Laroche's paper Planar 1-in-3 satisfiability is NP-complete. I couldn't get this paper, but most probably Laroche also meant positive by saying 'monotone'. Evenif he did not mean this, we can use Planar Positive 1-in-3 Satisfiability from Mulzer and Rote's paper Minimum-Weight Triangulation Is NP-Hard as the source problem instead.

See this answer for a question in cs.se