Paired resolution and $\mathsf{NP}$ vs. $\mathsf{coNP}$?

Let we resolve only two clauses at time and then get rid of them. Such resolution clearly takes $O(n)$ steps.

Sequence is a set of instructions in the form $(C_{S_1}\cup C_{S_2},v\cup\overline v),...$, where $S_i$ denotes a set of merged clauses, $v\in C_{S_1},\overline v\in C_{S_2}$.

Of course such resolution taken deterministically or randomly is wrong with high probability.

For example, let's consider $\varphi=(x\oplus y)(x\oplus z)(y\oplus z)$.

Clearly this formula is unsatisfiable. But what can I get using resolution:

$(x\oplus y)\Leftrightarrow(x\lor y)\land(\overline x\lor\overline y)$.

Resolving $x$ and $\overline x$: $(y\lor\overline y)=1$.

Doing this for other clauses gives us tautology.

So, this means, that sequence $(C_1\cup C_2,x\cup \overline x),(C_3\cup C_4,x\cup \overline x),(C_5\cup C_6,y\cup \overline y)$ is wrong.

But there is a correct sequence:$(C_1\cup C_4,x\cup\overline x),(C_2\cup C_3,\overline x\cup x),(C_{\{1,4\}}\cup C_5,\overline z\cup z),(C_{\{2,3\}}\cup C_6,z\cup\overline z),(C_{\{\{1,4\},5\}}\cup C_{\{\{2,3\},6\}},y\cup\overline y)$

Showing this:

Initial formula: $(x\lor y)(\overline x\lor\overline y)(x\lor z)(\overline x\lor\overline z)(y\lor z)(\overline y\lor\overline z)$

1. $(x\lor y)(\overline x\lor\overline z)\mapsto(y\lor\overline z)$
2. $(\overline x\lor\overline y)(x\lor z)\mapsto(\overline y\lor z)$
3. $(y\lor\overline z)(y\lor z)\mapsto y$
4. $(\overline y\lor z)(\overline y\lor\overline z)\mapsto\overline y$
5. $y\land\overline y\mapsto0$

There are exponentially many sequences for any formula. Same applies for number of possible assignments.

But what I'm asking: is such type of resolution is proved not to be refutation-complete? In other words have someone proved that not every unsatisfiable formula has a sequence that results in empty clause? Or is it an open question? (Otherwise we'd know that $\mathsf{NP=coNP}$)

P.S. This type of resolution is sound, so only thing that I do not know is refutation-completeness.

It is known that some formulas require exponentially long Resolution proofs. Therefore Resolution cannot be used (directly) to prove that $\mathsf{NP}=\mathsf{coNP}$.
• Proofs become exponential if we resolve all clauses simultaneosly. But here I resolve only 2 clauses at time. DTM still may require $\Theta(2^n)$ time to bruteforce them all. – rus9384 Sep 8 '17 at 12:02