The 3-SAT problem can be defined as follows:3-SATInput: 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 problemInput: 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?
Given a Boolean formula, does there exist a small circuit that computes a satisfying assignment?
cc.complexity theory;circuit complexity;sat;parameterized complexity;fine grained