The problem of deciding whether a monotone CNF implies a monotone DNF Consider the following decision problem

Input: A monotone CNF $\Phi$ and a monotone DNF $\Psi$.

Question: Is  $\Phi \to \Psi$ a tautology?

Definitely you can solve this problem in $O(2^n \cdot \mathrm{poly}(l))$-time, where $n$ is the number of variables in  $\Phi \to \Psi$ and $l$ is the length of input. On the other hand, this problem is coNP-complete. Moreover, a reduction which establishes coNP-completeness also shows that, unless SETH fails, there is no  $O(2^{(1/2 - \varepsilon)n} \mathrm{poly}(l))$-time algorithm for this problem (this holds for any positive $\varepsilon$). Here is this reduction. Let $A$ be a (non-monotone) CNF and let $x$ be its variable. Replace every positive occurence of $x$ by $y$ and every negative occurence of $x$ by $z$. Do the same for every variable. Let the resulting monotone CNF be $\Phi$. It is easy to see that $A$ is satisfiable iff $\Phi \to yz \lor \ldots $ is not a tautology. This reduction blows up the number of variables by a factor of 2, which implies $2^{n/2}$ (SETH-based) lower bound mentioned above. 

So there is a gap between $2^{n/2}$ and $2^n$-time. My question is whether any better algorithm or better reduction from SETH is known? 

Just two remarks seemingly related to the problem:


a reverse problem of whether a monotone DNF implies a monotone CNF is trivially solvable in polynomial time.
interestingly, the problem of deciding whether $\Phi$ and $\Psi$ compute the same function   can be solved in quasi-polynomial time due to Fredman and Khachiyan (On the Complexity of Dualization of Monotone Disjunctive Normal Forms, Journal of Algorithms 21 (1996), no. 3, pp. 618–628, doi: 10.1006/jagm.1996.0062)
Assuming SETH, the problem is not solvable in time $O\bigl(2^{(1-\epsilon)n}\mathrm{poly}(l)\bigr)$ for any $\epsilon&gt;0$.



First, let me show that this is true for the more general problem where $\Phi$ and $\Psi$ may be arbitrary monotone formulas. In this case, there is a poly-time ctt reduction from TAUT to the problem that preserves the number of variables. Let $T^n_t(x_0,\dots,x_{n-1})$ denote the threshold function
$$T^n_t(x_0,\dots,x_{n-1})=1\iff\bigl|\{i&lt;n:x_i=1\}\bigr|\ge t.$$
Using the Ajtai–Komlós–Szemerédi sorting network, $T^n_t$ can be written by a polynomial-size monotone formula, constructible in time $\mathrm{poly}(n)$.

Given a Boolean formula $\phi(x_0,\dots,x_{n-1})$, we may use De Morgan rules to write it in the form $$\phi'(x_0,\dots,x_{n-1},\neg x_0,\dots,\neg x_{n-1}),$$
where $\phi'$ is monotone. Then
$\phi(x_0,\dots,x_{n-1})$ is a tautology if and only if the monotone implications
$$T^n_t(x_0,\dots,x_{n-1})\to\phi'(x_0,\dots,x_{n-1},N_0,\dots,N_{n-1})$$
are valid for every $t\le n$, where
$$N_i=T^{n-1}_t(x_0,\dots,x_{i-1},x_{i+1},\dots,x_{n-1}).$$

For the left-to-right implication, let $e$ be an assignment satisfying $T^n_t$, i.e., with at least $t$ ones. There exists $e'\le e$ with exactly $t$ ones. Then $e'\models N_i\leftrightarrow\neg x_i$, thus $e'\models\phi$ implies $e'\models\phi'(x_0,\dots,x_{n-1},N_0,\dots,N_{n-1})$. Since this is a monotone formula, we also have $e\models\phi'(x_0,\dots,x_{n-1},N_0,\dots,N_{n-1})$. The right-to-left implication is similar.



Now, let me return to the original problem. I will show the following: if the problem is solvable in time $2^{\delta n}\mathrm{poly}(l)$, then for any $k$, $k$-DNF-TAUT (or dually, $k$-SAT) is solvable in time $2^{\delta n+O(\sqrt{kn\log n})}\mathrm{poly}(l)$. This implies $\delta\ge1$ if SETH holds.

So, assume we are given a $k$-DNF
$$\phi=\bigvee_{i&lt;l}\Bigl(\bigwedge_{j\in A_i}x_j\land\bigwedge_{j\in B_i}\neg x_j\Bigr),$$
where $|A_i|+|B_i|\le k$ for each $i$. We split the $n$ variables into $n'=n/b$ blocks of size $b\approx\sqrt{k^{-1}n\log n}$ each. By the same argument as above, $\phi$ is a tautology if and only if the implications
$$\tag{$*$}\bigwedge_{u&lt;n'}T^b_{t_u}(x_{bu},\dots,x_{b(u+1)-1})\to
\bigvee_{i&lt;l}\Bigl(\bigwedge_{j\in A_i}x_j\land\bigwedge_{j\in B_i}N_j\Bigr)$$
are valid for every $n'$-tuple $t_0,\dots,t_{n'-1}\in[0,b]$, where for any $j=bu+j'$, $0\le j'&lt;b$, we define
$$N_j=T^{b-1}_{t_u}(x_{bu},\dots,x_{bu+j'-1},x_{bu+j'+1},\dots,x_{b(u+1)-1}).$$
We can write $T^b_{t}$ as a monotone CNF of size $O(2^b)$, hence the LHS of $(*)$ is a monotone CNF of size $O(n2^b)$. On the right-hand side, we may write $N_j$ as a monotone DNF of size $O(2^b)$. Thus, using distributivity, each disjunct of the RHS can be written as a monotone DNF of size $O(2^{kb})$, and the whole RHS is a DNF of size $O(l2^{kb})$. It follows that $(*)$ is an instance of our problem of size $O(l2^{O(kb)})$ in $n$ variables. By assumption, we may check its validity in time $O(2^{\delta n+O(kb)}l^{O(1)})$. We repeat this check for all $b^{n'}$ choices of $\vec t$, thus the total time is
$$O\bigl((b+1)^{n/b}2^{\delta n+O(kb)}l^{O(1)}\bigr)=O\bigl(2^{\delta n+O(\sqrt{kn\log n})}l^{O(1)}\bigr)$$
as claimed.



We get a tighter connection with the (S)ETH by considering the bounded-width version of the problem: for any $k\ge3$, let $k$-MonImp denote the restriction of the problem where $\Phi$ is a $k$-CNF, and $\Psi$ is a $k$-DNF. The (S)ETH concerns the constants
$$\begin{align*}
s_k&amp;=\inf\{\delta:k\text-\mathrm{SAT}\in\mathrm{DTIME}(2^{\delta n})\},\\
s_\infty&amp;=\sup\{s_k:k\ge3\}.
\end{align*}$$
Likewise, let us define
$$\begin{align*}
s'_k&amp;=\inf\{\delta:k\text-\mathrm{MonImp}\in\mathrm{DTIME}(2^{\delta n})\},\\
s'_\infty&amp;=\sup\{s'_k:k\ge3\}.
\end{align*}$$
Clearly,
$$s'_3\le s'_4\le\dots\le s'_\infty\le1$$
as in the SAT case. We also have
$$s'_k\le s_k,$$
and the double-variable reduction in the question shows
$$s_k\le2s'_k.$$
Now, if we apply the construction above with constant block-size $b$, we obtain
$$s_k\le s'_{bk}+\frac{\log(b+1)}b,$$
hence
$$s_\infty=s'_\infty.$$
In particular, SETH is equivalent to $s'_\infty=1$, and ETH is equivalent to $s'_k&gt;0$ for all $k\ge3$.