Polynomial kernel for $k$-FLIP SAT on $3$-CNF formulas The k-FLIP SAT parametrized problem is defined as:

Input: a 3-CNF formula $\varphi$ with $n$ variables and a truth assignment $\sigma : [n] \to \{0,1\}$
Parameter: $k$
Question: can we transform the assignment $\sigma$ into a satifying assignment $\sigma'$ for $\varphi$ flipping the truth value of at most $k$ variables? 

The problem is clearly in FPT (Stefan Szeider: The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT. Discrete Optimization 8(1): 139-145 (2011)) 


  Does it admit a polynomial kernel ? (under reasonable complexity assumptions)


The recent cross-composition techniques (see Hans L. Bodlaender, Bart M. P. Jansen, Stefan Kratsch, "Kernelization Lower Bounds By Cross-Composition") seem unuseful for this problem. And they also seem unuseful for similar problems that ask if a given solution to an NP-hard problem can be found from a given instance by local search (limiting the search to the neighbours of the given instance, under some natural distance measure).
The problem does not have a polynomial kernel unless NP is in coNP/poly. The cross-composition technique from our paper applies in a nontrivial way.

Let me show how the classic Vertex Cover problem OR-cross-composes into the k-FLIP-SAT problem; by the results in the cited paper, this is sufficient. Concretely, we build a polynomial-time algorithm whose input is a sequence of Vertex Cover instances $(G_1,k), (G_2, k), \ldots, (G_t, k)$ that all share the same value of $k$ and all have exactly $n$ vertices. The output is an instance of $k$-FLIP SAT with a parameter value of $O(k + \log t)$, which is sufficiently small for a cross-composition, such that the $k$-FLIP SAT instance has answer yes iff one of the input graphs has a vertex cover of size $k$. By duplicating one input (which does not change the value of the OR) we can ensure that the number of inputs $t$ is a power of two.

The composition proceeds as follows. Number the vertices in graph each input graph $G_i$ as $v_{i,1}, v_{i,2}, \ldots, v_{i,n}$. Make a corresponding variable in the FLIP-SAT instance for each vertex of each input graph. Additionally, make a selector variable $u_i$ for each input instance number $i \in [t]$. For each input graph $G_i$, we add some clauses to the formula. For each edge $\{v_{i,x}, v_{i,y}\}$ of graph $G_i$, add the clause $(v_{i,x} \vee v_{i,y} \vee \neg u_i)$ to the formula, which will encode "either one of the endpoints of this edge is set to true, or the instance $i$ is not active". In the initial assignment, all vertex-variables are set to false and all selector variables $u_i$ are set to false, so that these clauses are all satisfied. To build the OR-behavior into the composition we will augment the formula to ensure that a satisfying assignment sets at least one selector to true, and must then also form a vertex cover of the selected graph.

To make sure we can do this selection while keeping the flip distance small compared to the number of inputs $t$, we use the structure of a complete binary tree with $t$ leaves, which has height $\log t$. Number the leaves from $1$ to $t$ and associate the $i$-th leaf with the variable $u_i$ that controls if input $i$ is active or not. Create a new variable for each internal node of the binary tree. For each internal node, let its corresponding variable be $x$ and the variables of its two children be $y$ and $z$. Add the clause $(\neg x \vee y \vee z)$ to the formula which captures the implication $(x \rightarrow (y \vee z))$, enforcing that $x$ can only be true if one of its children is true. To complete the formula, add a singleton clause saying that the variable of the root node of the binary tree must be true. In the initial truth assignment, the values of all variables for internal nodes is set to false, which satisfies all clauses of the formula except for the singleton clause requiring the root node of the tree to have its variable true.

This completes the description of the formula and truth assignment. Set the parameter $k'$ of the FLIP DISTANCE problem to be equal to $(k + \log t + 1)$, which is suitably bounded for a cross-composition. It remains to show that we can flip $k'$ variables to make the formula true iff some input graph $G_i$ has a vertex cover of size $k$.

In the reverse direction, suppose that $G_i$ has a size-$k$ vertex cover. Set the $k$ variables corresponding to the $k$ vertices in the cover to true by flipping them. Set the selector variable $u_i$ to true to encode that input $i$ is activated, and flip the variables of the $\log t$ internal binary tree nodes on the path of leaf $i$ to the root to true. It is easy to verify that this is a satisfying assignment: the implications in the binary tree are all satisfied, the root node's value is set to true, the clauses that check edges of $G_{i'}$ for $i' \neq i$ remain satisfied because $u_{i'}$ remains false, while the clauses for graph $G_i$ are satisfied because for every edge we set at least one endpoint to true.

For the forward direction, suppose that the formula can be satisfied by flipping at most $k + \log t + 1$ variables. Then we must flip the variable of the root node to true. The implications in the binary tree enforce that at least one selector variable of a leaf is set to true, say $u_i$. To satisfy the implications encoded in the binary tree, all internal nodes on the path from $u_i$ to the root were set to true, accounting for $1 + \log t$ flips. Since $u_i$ is set to true, the clauses made for graph $G_i$ are not satisfied on the literal $\neg u_i$, so they are satisfied because one of the endpoints of each edge of $G_i$ is set to true. Since at least $1 + \log t$ variables of the binary tree were flipped, at most $k$ vertex-variables are flipped to true in this solution. This encodes a vertex cover of size $k$ in $G_i$ and proves that one of the inputs is a YES-instance. This completes the proof.