The 3-SAT problem can be defined as follows:
Input: A 3-CNF formula $\phi$ of size $m$ with $n$ variables.
Question: Does there exist a variable assignment that satisfies $\phi$?
Consider the following parameterized problem that is a variantion of 3-SAT:
CVA: Compressed variable assignment problem
Input: A number $k$ and a 3-CNF formula $\phi$ of size $m$ with $n$ variables.
Question: Does there exist a circuit $C$ of size at most $k\log(n)$ that computes a variable assignment that satisfies $\phi$?
Note: By circuit size, I mean the number of bits in the circuit's binary encoding where the circuits have bounded fan-in.
Below I will share some questions and results about the CVA problem.
Question 1: Do you happen to have any references to this problem or know of any related variants of SAT?
Question 2: How quickly can we solve the CVA problem in terms of parameters $m$, $n$, and $k$?
The brute force approach for solving this problem is to enumerate all circuits of size $k\log(n)$ and compute their corresponding assignments. For each assignment, we check if it satisfies $\phi$. This should take roughly $m \cdot n^k \cdot k\log(n)$ time.
Question 3: What is the parameterized complexity of this problem? How does it relate to other parameterized problems, the $W$ hierarchy, and other complexity classes?
It's worth noticing that the CVA problem is harder than a variation of the minimum circuit size problem found here: Parameterized complexity of deciding if a string can be computed by circuits of size $k\log(n)$
In particular, given a number $k$ and a bit string $x$, we can build a trivial 1-SAT formula $\phi$ that is only satisfied by $x$. Then, $x$ can be computed by a circuit of size $k\log(n)$ if and only if $\phi$ has a satisfying assignment that can be computed by a circuit of size at most $k \log(n)$.
Question 4: Does looking at compressible satisfying assignments have any practical significance? Has anyone ever measured the compression ratio of satisfying assignments for a collection of SAT instances that have come up in practice?