Reference request: complexity of $k$-partite $k$-SAT

Question

Let's consider following variation of $k$-SAT that I will call $k$-partite $k$-SAT:

given $n$ variables that are divided into $k$ groups and a $k$-SAT formula $\phi$ such that each clause has literal from each group. Is $\phi$ satisfiable?

There is an almost straightforward reduction from $k$-SAT to $k$-partite $k$-SAT that takes formula on $n$ variables and produces formula on $kn$ variables. This proves that this problem is exponentially hard under $ETH$.

On the other hand there a very simple $O^*(2^{(1-\frac{2}{k})n})$ time algorithm for this problem: branch over all variables except 2 groups. You will end up with $2$-SAT problem, that can be solved in polynomial time.

As we don't know algorithms with this kind of savings for $k$-SAT, I'd be surprised if there is a simple reduction from $k$-SAT to $k$-partite $k$-SAT that preserves number of variables.

So I have following question:

• Was this problem studied before?
• Is there an algorithm with running time $O^*(2^{(1-\epsilon)n})$, where $\epsilon$ is independent on $k$?
• If answer for previous question is no, do we know that complexity goes to $2^n$ as $k$ goes to infinity under $SETH$?

Answer 1

Claim: If there exists an $\epsilon > 0$ such that for every $k'$, $k'$-partite $k'$-SAT can be solved in $2^{n(1-\epsilon)}$ time, then SETH fails.

Proof: Suppose such an algorithm exists. We give an algorithm that, for every $k$ solves $k$-SAT in time $2^{n(1-\epsilon/2)}$. Consider a $k$-SAT instance with $n$ variables, apply the sparsification lemma so that it produces $2^{n(\epsilon/2)}$ instances where, in every instance, every variable occurs in at most $(k/\epsilon)^{O(k/\epsilon)}$ clauses. Each of these instances are $(k/\epsilon)^{O(k/\epsilon)}$-partite in the sense that one can find a coloring of the variables into $k' = (k/\epsilon)^{O(k/\epsilon)}$ colors such that no clause contains variables with the same color. If you want clauses of size exactly $k'$ you can replace clauses of size $k$ by $2^{k'-k}$ clauses of size $k'$. Running the $2^{n(1-\epsilon)}$ time algorithm on each of the $2^{n(\epsilon/2)}$ instances of $k'$-partite $k'$-SAT gives an algorithm for $k$-SAT with running time $2^{n(1-\epsilon/2)}$ as claimed.

Note that the above proof essentially reduces $k$-SAT to $k^k$-partite $k^k$-SAT. So an algorithm with running time $2^{n(1-\frac{\log \log k}{\log k})}$ could still be possible, if very surprising.