Let's try to solve "co3SAT" with an NTM in polynomial time. It seems we need, more or less, to guess a proof that the formula is unsatisfiable i.e. derive a contradiction.

We've got a formula in conjunctive normal form, a big AND of OR clauses, each clause with 3 literals. Let's suppose we adopt the following strategy: at each stage, we expand two of of the clauses using the distributive law (AND distributes over OR), and simplify the result whenever possible. In the end, if the formula is unsatisfiable, we should get "false" from this procedure.

Is a lower bound known for this procedure (i.e. is it known whether this necessarily uses exponential time, given that we can use the non-determinism to select the optimal order in which the clauses are expanded)?

I read a little a bit about lower bounds for resolution techniques using the pigeonhole principle, but at first glance this seems like a different problem.

  • $\begingroup$ De Morgan's laws state that $\overline{A \lor B} = \overline{A} \land \overline{B}$ and $\overline{A \land B} = \overline{A} \lor \overline{B}$. What you mention is just the distributive law. $\endgroup$ Jan 11 '16 at 16:25
  • 1
    $\begingroup$ Your title is a bit too general. Try to find something more specific. $\endgroup$ Jan 11 '16 at 16:27
  • 2
    $\begingroup$ You are claiming to have a solution for a well-known, difficult open problem. This is an extraordinary claim requiring extraordinary evidence. You have not provided such so there is not much to talk about. Even if you had, this would not be a good post for SE; it is not our goal here to make broad advances to science in a single post. See here for a related discussion. $\endgroup$
    – Raphael
    Jan 11 '16 at 19:32
  • $\begingroup$ No, I'm not making any claims at all. Perhaps the title of my post was misleading. I was asking whether a lower bound is known for a certain approach -- that's hardly the same thing as claiming to have a solution. $\endgroup$
    – Brian
    Jan 12 '16 at 8:37

It is not known whether NP=coNP or NP≠coNP, but the latter is strongly suspected. It is not even known whether P≠NP implies NP≠coNP.

It is known that NP≠coNP implies P≠NP, and this approach for proving P≠NP is known as "Cook's program".

Now to your particular proof system. As far as I understand, your proof system maintains a collection of DNFs, which are initially the clauses of the original CNF (so they are trivial DNFs in the sense that all terms have width 1). At each step, you take two DNFs and combine them to a new DNF.

This system is similar to "depth-2 Frege", which is the following system. You start with "axioms" which are the clauses of the original CNF that you are trying to refute. The proof consists of a sequence of "lines" (propositions), each one either an axiom or following from previous lines via one or more derivation rules. In addition, all the lines are constrained to be formulas of depth 2 (CNFs or DNFs). The exact choice of derivation rules doesn't matter - fix any finite set of derivation rules of your choice.

It seems that one can simulate your proof system using depth-2 Frege in such a way that the number of lines in the Frege proof is comparable to the size of your proof. To know for sure, one needs to examine the exact simplification rules that you use, and show how to simulate them using depth-2 Frege. I believe that this should work out.

The pigeonhole principle is hard not only for Resolution, but also for bounded depth Frege. In particular, refuting the pigeonhole principle using depth-2 Frege takes $2^{n^{\Omega(1)}}$ lines, where $n$ can be taken as the size of the formula. See for example Fu and Urquhart.

  • $\begingroup$ 1. Expand (x1 or y1) and not x1 --> (x1 and not x1) or (y1 and not x1) --> (y1 and not x1). 2. Expand (y1 and not x1) and not y1 --> y1 and not x1 and not y1 --> contradiction, since y1 and not y1 $\endgroup$
    – Brian
    Jan 12 '16 at 9:06
  • $\begingroup$ Now I'm not sure I understand your procedure. $\endgroup$ Jan 12 '16 at 9:17
  • $\begingroup$ In the case you mentioned, where you have (A1 or ... or Aa) and (B1 or ... or Bb), this is an "and" with two clauses. The final simplification results in a big "or" with no further simplifications, so you're finished. The formula is satisfiable. After the first step, the formula is no longer in CNF - it is a conjunction of disjunctions of conjunctions of literals. At each stage, the number of outer "ands" goes down by one. $\endgroup$
    – Brian
    Jan 12 '16 at 9:27
  • $\begingroup$ With satisfiable formulas, it is known that you can have exponential blow up with this procedure -- I'm wondering if anything is known on the unsatisfiable side. $\endgroup$
    – Brian
    Jan 12 '16 at 9:28
  • $\begingroup$ It's very hard to answer that since I don't understand your procedure. Please give a concrete, non-trivial example of your procedure. $\endgroup$ Jan 12 '16 at 9:32

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.