# CNF encoding of set cover - NExpTime-completness

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...