1

these are some probably very hard but possibly significant and deep questions related to an unusual but intriguing possible "recursive" construction/formulation in SAT, with some important "structure" or "dynamics" not previously considered. do not expect definitive answers in the short term but am sharing in a preliminary/sketchy form & maybe somebody in cyberspace/TCS will find it interesting also.

consider a resolution based proof for a set of SAT clauses. that resolution proof is in the form of a 2-indegree DAG (or in special cases, a tree) where the leaf nodes are clauses, and every node has 2 "ancestors". (this is potentially very interesting though because circuits are usually/often represented as DAGs and can be and are also converted to 2-indegree.)

can arbitrary/all 2-indegree DAGs be represented by SAT resolution proofs based on selecting particular/specially constructed/contrived SAT instances? in other words, given an arbitrary 2-indegree DAG, are there clauses that "generate" it in the corresponding resolution (refutation?) proof, and if so, what are they? and also what are the minimal clauses that do so?

(of course a resolution DAG could be either for a proof or a refutation proof. am not specifying/fixing that for this above question. also minimal is not yet/further defined. it could be either "length" (number) or "width" (number of variables) of the SAT instance, or some combination or maybe some other meaningful/natural measure.)

it feels like it could be used in a (important?) proof, eg possibly for complexity class separation via diagonalization, somehow, someday. am working on a further/related possibly remarkable construction that requires a "yes" answer ie that all 2-indegree DAGs are possible. (hope to post further on that later.)

these do seem to be fundamental yet novel, not-previously considered questions based on the literature. "nearby" refs could be useful. my intention will be to upvote and/or accept any partial but intelligent answers & encourage others to follow.

vzn
  • 11,014
  • 2
  • 31
  • 64
  • This seems to be a post for sharing ideas and soliciting opinions about them, not a real question. Please use a blog if you want to share your ideas and discuss them. I am closing this as not a real question. – Kaveh Feb 17 '13 at 01:01
  • 2
    Ps: in resolutions proof system, proofs are always refutation proofs, so I should say that as someone working in proof complexity I don't understand what you are talking about here. It seems to me that you don't know what you are talking about. – Kaveh Feb 17 '13 at 01:23
  • 6
    Despite the rambling, badly formatted, somewhat pompous text, I think there is a clear question here: Can every finite DAG in which nodes have in-degree 0 or 2 arise as the structure of a resolution derivation. – Vijay D Feb 17 '13 at 01:38
  • @Kaveh, I'm not sure I agree. Isn't resolution a sound but incomplete deduction system, besides being refutation complete? Meaning, if I can derive a clause C from A and B by resolution, then "A and B implies C" is a propositional tautology. I believe resolution proofs, as opposed to refutations, appear in the literature, for example to formalise learning in SAT solvers (independent of whether a formula is UNSAT, learning has a resolution formulation). – Vijay D Feb 17 '13 at 01:41
  • 2
    @VijayD I don't think it gives much insight. In any case the answer is positive if I am not making a mistake: turn it into a tree, use Res only once on each variable, turn it back into dag by merging. – Kaveh Feb 17 '13 at 01:49
  • not following. which was the pompous sentence? resolution proofs lead either to a solution or a derivation of a contradiction, whats the confusion on that? others have criticized at other times for not providing "background"... not sure what the assertion "all proofs are refutation proofs" comes from & it doesnt make sense to me... as for typically-heavyhanded/unilateral k's inability to read the highlighted question, have no "answer" to that... – vzn Feb 17 '13 at 01:52
  • @VijayD, of course you can use resolution that way but in logic, complexity, and proof complexity, AFAIK, that is not the case, resolution proof means refutation proof. – Kaveh Feb 17 '13 at 02:05
  • ?? resolution is complete for 1st order logic.. it is basically the method used in DPLL solvers to find either solutions or prove the formula is unsatisfiable. this is logic 101... – vzn Feb 17 '13 at 02:13
  • 1
    @vzn, what I understand from your first paragraph, this is definitely not a real question. The fact that you have included a question does change that fact. If your intention is to question that VijayD says please remove the rest and we will consider reopening it. This site is for asking answerable question, not discuss, share ideas, make claims, or suggest approaches. For those purposes use a blog post. – Kaveh Feb 17 '13 at 04:02
  • 1
    ps: I agree with VijayD, it is pompous to make such claims as you do here about topics that you are not an expert. – Kaveh Feb 17 '13 at 04:04
  • 4
    I don't understand why it got closed. I can understand commenting on this and suggesting improvements, and even downvoting. But not closing. It got 2 upvotes and 3 faves as well. @vzn can you edit as suggested by VijayD ? – Suresh Venkat Feb 17 '13 at 04:42
  • @Surresh, this is the second time that we have a disagreement recently. Previously you objected to my down-voting an answer by OP. It seems to me the core issue here is the same as there. My down-vote was of course a personal decision. However this one is a moderation issue so I think it would be good to discuss it on meta and agree on a how to deal with this. I have started a meta-discussion about this. – Kaveh Feb 17 '13 at 07:33
  • what is the "pompous claim"? all assertions are tentative & labelled honestly as such. feel free to disprove me with actual rigorous TCS/MATHEMATICS. does anyone wanna write about TCS instead of @#$%& trivial META? – vzn Feb 17 '13 at 23:14
  • 6
    If you describe your own question as "very hard", "deep", "significant" it comes across as pompous, independent of using weasly qualifiers such as "probably" and "possibly". You can improve the question by deleting the first and last paragraph and consulting the reformulation I suggest in meta. If you make the question rigorous, we may respond with a rigorous answer. – Vijay D Feb 18 '13 at 05:25
  • @vijay its a veiled warning that the question is maybe difficult and unlikely to have a snap answer, which frankly, means its intrinsically not a good fit for the stackexchange network, but then again, maybe cstheory with its narrow aims is not really a very good fit for it either.... as for qualifiers, they are legitimate words in the english language and used routinely in scientific papers as anyone who reads them regularly will agree/recognize.... as for your meta reformulation, like it, but unless you have the cojones to put it on the main site (like I did above), ghettoized – vzn Feb 18 '13 at 05:34

1 Answers1

5

Let's assume that you do not allow Tautologies in the leafs, and consider a structure where exactly 3 leafs have edges to a node $A$. Denote the leaf clauses by $(a\vee L_1),(\neg a\vee b\vee L_2),(\neg b\vee L_3)$, where $L_1,L_2,L_3$ are discunctions of literals. Since they all have edges to $A$, we have the following: Leaves 1,2 resolve to $(b\vee L_1\vee L_2)$. Leaves 2,3 resolve to $(\neg a\vee L_2\vee L_3)$

Since $A$ is a single node, then these expressions are equal. Since there is no initial tautology, then $b\notin L_3$, but this implies that $b\in L_2$, which isn't the case (assume we have no duplicates).

So the only possibility is $b=\neg a$, but this means that $L_1=L_2\vee L_3$ and $L_3=L_2\vee L_3$, so the leaves aren't distinct.

If I am not mistaken, then this means that this structure is not possible, so not every DAG is possible (under the assumptions).

Shaull
  • 5,571
  • 1
  • 22
  • 32
  • is this a proof that there exist DAGs with more than 3 edges into a node that cant be Resolution proofs? sorry, realize, need to modify the question for that case. all resolution proofs of course are "2-descendant" DAGs – vzn Feb 16 '13 at 17:28
  • Technically you can get any even degree, depending on whether you distinguish identical nodes formed from different clauses. – Shaull Feb 16 '13 at 17:33
  • that should read "3 or more". "degree" is defined for undirected graphs, but what is "degree" defined as on a DAG? guess you mean "indegree"? anyway, related question, if not all 2-descendant (2-indegree) DAGs are possible (not convinced of this yet), what characterizes the resolution-based DAG class? is it considered elsewhere? etc. – vzn Feb 16 '13 at 17:50
  • Indeed, I meant in-degree. – Shaull Feb 16 '13 at 18:03
  • fyi, am accepting this answer because the question was (unfairly) closed & there is no opportunity for new, complete, creative etc. answers – vzn Feb 17 '13 at 23:16