CNF encoding of set cover - NExpTime-completness

Question

Notation: given a CNF formula A over variables X, we write $[A(X)]$ for the set of valuations $v: X \to \{0,1\}$ such that $A(X/v)$ is true, i.e. the set of valuations that makes formula A true.

I suspect that the following problem is NExpTime-complete:

-given two CNF formulas $A(X)$ and $B(Y,X)$, and an integer $K=2^k$, determine if there exist $K$ valuations $v_1,v_2,...,v_K : Y \to {0,1}$ such that $[A(X)] \subseteq \bigcup_{v=v_1,v_2,...,v_K} [B(Y/v,X)]$, i.e. are there K valuations of the variables in Y such that all the valuations that makes $A(X)$ true are covered by valuations that makes $B(Y/v,X)$ true.

So this can be seen as a succinct encoding of the set cover problem using CNF formulas. My guess is that this result should be a consequence of the NP completness of set cover and some general results about succinct encodings of problems using CNF formulas. Unfortunately, I was not able to locate such a result in the literature...

Answer 1

As I suspected in my question, they are useful results in the literature that can be exploited to characterize the complexity of the problem. There is a reduction from the dominant set problem for graphs succinctly defined using CNF formulas to the problem that I have described. The dominant set problem is known to be NExpTime complete [1] for graph succinctly defined using CNF formulas.

An instance of DominantSet^{2^n}{CNF} is defined by an CNF formula E(X,Y) over X={x_1,x_2,…,x_n} and Y={y1,y2,…,y_n}, two sets of n Boolean variables, and an integer K (encoded in binary) . The formula E(X,Y) succinctly defines the following graph: the set of vertices is the set of all Boolean valuations over n variables: 2^n, so any valuation v for the set of variables X, or for the set of variables Y, defines a vertex. Let v_1 and v_2 be two such valuations, then there is an edge={v_1,v_2} in the graph iff E(v_1,v_2) is true or E(v_2,v_1) is true. An instance is positive, if there exists a set of K valuations V={v_1,v_2,…,v_K} such that \cup{v \in V} { v’ | E(v,v’) \lor E(v’,v) }=2^n (i.e. all vertices are adjacent to a vertex in V).

We can reduce in polynomial time this problem to our succinct set cover problem as follows:

Define 𝐴(U) to be the empty CNF formula over the set of n variables U (which is equivalent to true) and so [A(U)]=2^n. Then define B(Z,U) to be the CNF equivalent to E(Z,U) \lor E(U,Z). This last formula has a size which is polynomial in the size of the CNF E that defines the graph. Keep K unchanged.

Then it is direct to see that the instance of succinct set cover is positive iff the DominantSet instance is positive. Indeed, there is a set V of K valuations for the variables in Z such that \bigcup_{v \in V} { v' | B(v,v') } covers 2^n iff V is a dominant set.

[1] Patrick Schafenacker. Problems on succinctly encoded graphs. PhD dissertation. Universität Ulm 2017.