# A SAT related question

Given a sequence of $n$ propositional formulas $\varphi_1, \cdots, \varphi_n$, a propositional formula $\phi$, a number $1\leq \theta\leq n$.

Define $K=\min\{k\mid \wedge_{i=k}^n \varphi_i\not\models \phi\}$, i.e., it is the minimal number $k$ such that the conjunction of $\varphi_k, \cdots, \varphi_n$ does not imply $\phi$.

Question: what's the complexity of deciding whether $K=\theta$?

What I have tried: Since deciding $\wedge_{i=k}^n\varphi_i\not\models \phi$ is NP-complete, this problem is in $P^{NP}$. Moreover, by binary search, this can be improved to $\Theta^p_2$, i.e., only logarithmic number of NP queries is enough. (Is this correct?) However, I am not clear about the lower bound. Maybe it is just in NP?

• You only need to test $\theta$ and $\theta+1$, so the problem is in DP. It’s not difficult to prove that it’s actually DP-complete. – Emil Jeřábek Jul 17 '15 at 12:01
• I mean $\theta$ and $\theta-1$. – Emil Jeřábek Jul 17 '15 at 12:15
• Thanks. I am not familiar with DP, so could you please outline the DP-hardness? – maomao Jul 17 '15 at 13:28
• @NieldeBeaudrap Note that the intersection is pointwise. And you probably mean $\mathsf{BH}_2$. – Cornelius Brand Jul 18 '15 at 14:16