Does every NO instance of this promise problem have a local refutation? For the following equivalent questions, you choose

whether-or-not the 3 variables in a clause must be distinct.


  Is there an integer $k$ such that for all 3-SAT formulas $\mathcal{F}$ without negations,
  
  if every ​ $(\leq k)$-clause sub-formula of $\mathcal{F}$ is 1-in-3 satisfiable then $\mathcal{F}$ is NAE-satisfiable?
  
  Equivalently, is there an integer $k$ such that for all
  
  3-SAT formulas $\mathcal{F}$ without negations, if $\mathcal{F}$ is not NAE-satisfiable then
  
  $\mathcal{F}$ has a ​ $(\leq k)$-clause sub-formula which is not 1-in-3 satisfiable?


(The Fano plane shows that $k$ can't be less than $7$.)


Motivation: ​ ​ ​ That is the "low end" of my question

on cs.stackexchange which was inspired by the

possibility of generalizing Schaefer's dichotomy theorem

to constraint satisfaction promise problems.

Specifically, for the simplest non-trivial promise-constraint,

with m being the size of the input set, I have neither managed to

find evidence for it being in ​ promisecoQIP[2]TIME$\hspace{-0.02 in}\big(\hspace{-0.04 in}$2o(m)$\hspace{-0.03 in}\big)\hspace{-0.04 in}\big/\hspace{-0.04 in}$q2o(m)

for infinitely many m, nor find evidence that it's not solvable

in coNTIME(O(1)) on essentially the most basic word RAM.

The former applies even when each variable occurs exactly twice

and "many m" gets replaced with "many even m" (since 3 is odd),

and the latter applies even when negative literals are allowed.
So if I understood well, your problem in the language of graph theory would be as follows:


  Is there a $k$ such that if for a $3$-uniform hypergraph for any $k$ of its edges we can select a $1$-shallow hitting set (a set of vertices that meets each of the $k$ edges in exactly one vertex), then the hypergraph is $2$-colorable?


The answer to this question is no because for any $g$ and $r$ there are $r$-uniform hypergraphs of girth $g$ with arbitrarily high chromatic number [Kostochka-Nesetril].
The girth $g$ of an $r$-uniform hypergraph is the smallest $g$ for which there are $g-1$ edges whose union has size at most $g(k-1)$.
Thus, if a hypergraph has girth $g$, then any $g-1$ edges have a $1$-shallow hitting set by induction because their union looks like a tree.
This means that locally it satisfies your 1-in-3 satisfiability condition, but it is not $2$-colorable, so there is no NAE-satisfying assignment for the whole hypergraph.