1
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

It is known that some formulas require exponentially long Resolution proofs. Therefore Resolution cannot be used (directly) to prove that $\mathsf{NP}=\mathsf{coNP}$.

Note that the details of your procedure are completely irrelevant. The lower bounds show that whatever algorithm you use to create your Resolution refutations, there will be some formulas on which it will take exponential time, simply because every Resolution refutation of these formulas is exponentially long.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – rus9384 Sep 8 '17 at 12:02
  • $\begingroup$ There are formulas for which every Resolution refutation contains exponentially many clauses. No way around it. $\endgroup$ – Yuval Filmus Sep 8 '17 at 12:02
  • $\begingroup$ So, this type of resolution does not refuse all unsatisfiable formulas? $\endgroup$ – rus9384 Sep 8 '17 at 12:05
  • 1
    $\begingroup$ Any type of Resolution which uses at most a polynomial number of steps (each step consisting of resolving two clauses) is not refutation-complete. $\endgroup$ – Yuval Filmus Sep 8 '17 at 12:20
  • $\begingroup$ Well, I tried to check it on smallest Tseitin contradiction and yes, it's only possible if we use each clause, since we must get a full CNF. $\endgroup$ – rus9384 Sep 8 '17 at 13:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.