<p>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)$</p>

<p>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).</p>

<p>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.</p>

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

CC BY-SA 3.0
2013-02-16T17:28:14.280Z
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
CC BY-SA 3.0
2013-02-16T17:33:18.530Z
Technically you can get any even degree, depending on whether you distinguish identical nodes formed from different clauses.
Shaull
CC BY-SA 3.0
2013-02-16T17:50:35.367Z
that should read "3 or more". ["degree"](http://en.wikipedia.org/wiki/Degree_(graph_theory)) is defined for undirected graphs, but what is "degree" defined as on a DAG? guess you mean ["indegree"](http://en.wikipedia.org/wiki/Indegree#Indegree_and_outdegree)? 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
CC BY-SA 3.0
2013-02-16T18:03:50.763Z
Indeed, I meant in-degree.
Shaull
CC BY-SA 3.0
2013-02-17T23:16:13.810Z
fyi, am accepting this answer because the question was **(unfairly) closed** & there is no opportunity for new, complete, creative etc. answers
vzn
CC BY-SA 3.0
2013-02-16T17:16:19.183Z
2013-02-16T17:16:19.183Z
Shaull
<p>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 &amp; maybe somebody in cyberspace/TCS will find it interesting also. </p>

<p>consider a resolution based proof for a set of SAT clauses. that resolution proof is in the form of a <em>2-indegree</em> 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.)</p>

<blockquote>
  <p>can <em>arbitrary/all</em> 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 <em>minimal</em> clauses that do so?</p>
</blockquote>

<p>(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 <em>minimal</em> 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.)</p>

<p>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.) </p>

<p>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 &amp; encourage others to follow.</p>

CC BY-SA 3.0
2013-02-17T01:01:03.470Z
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
CC BY-SA 3.0
2013-02-17T01:23:35.287Z
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
CC BY-SA 3.0
2013-02-17T01:38:14.117Z
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
CC BY-SA 3.0
2013-02-17T01:41:54.117Z
@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
CC BY-SA 3.0
2013-02-17T01:49:14.533Z
@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
CC BY-SA 3.0
2013-02-17T01:52:55.950Z
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
CC BY-SA 3.0
2013-02-17T02:05:48.933Z
@VijayD, of course you can use resolution that way but in logic, complexity, and proof complexity, AFAIK, that is not the case, [resolution proof](http://en.m.wikipedia.org/wiki/Resolution_(logic)) means refutation proof.
Kaveh
CC BY-SA 3.0
2013-02-17T02:13:27.023Z
?? [resolution is complete for 1st order logic.](http://en.wikipedia.org/wiki/First-order_logic#Resolution). it is basically the method used in [DPLL](http://en.wikipedia.org/wiki/DPLL_algorithm) solvers to find either solutions or prove the formula is unsatisfiable. this is logic 101...
vzn
CC BY-SA 3.0
2013-02-17T04:02:08.630Z
@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
CC BY-SA 3.0
2013-02-17T04:04:47.270Z
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
CC BY-SA 3.0
2013-02-17T04:42:05.253Z
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
CC BY-SA 3.0
2013-02-17T07:33:53.127Z
@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](http://meta.cstheory.stackexchange.com/q/2653/186) about this.
Kaveh
CC BY-SA 3.0
2013-02-17T23:14:37.167Z
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
CC BY-SA 3.0
2013-02-18T05:25:17.103Z
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
CC BY-SA 3.0
2013-02-18T05:34:42.977Z
@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
<cc.complexity-theory><reference-request><graph-theory><proofs><np-complete>
in SAT resolution proofs, are all DAGs possible?
vzn
# in SAT resolution proofs, are all DAGs possible?

(Asked by: username_0 on 2013-02-16)

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.

**Tags:** cc.complexity-theory, reference-request, graph-theory, proofs, np-complete

> **Comments:**
> **username_1**: 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.  
> **username_1**: 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.  
> **username_2**: 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.  
> **username_2**: @username_1, 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).  
> **username_1**: @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.  
> **username_0**: 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...  
> **username_1**: @VijayD, of course you can use resolution that way but in logic, complexity, and proof complexity, AFAIK, that is not the case, [resolution proof](http://en.m.wikipedia.org/wiki/Resolution_(logic)) means refutation proof.  
> **username_0**: ?? [resolution is complete for 1st order logic.](http://en.wikipedia.org/wiki/First-order_logic#Resolution). it is basically the method used in [DPLL](http://en.wikipedia.org/wiki/DPLL_algorithm) solvers to find either solutions or prove the formula is unsatisfiable. this is logic 101...  
> **username_1**: @username_0, 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.  
> **username_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.  
> **username_3**: 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. @username_0 can you edit as suggested by VijayD ?  
> **username_1**: @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](http://meta.cstheory.stackexchange.com/q/2653/186) about this.  
> **username_0**: 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**?  
> **username_2**: 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.  
> **username_0**: @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_  

---

## 1 answers

### Answer by username_4 on 2013-02-16. Score: 5 | Accepted answer

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).

> **Comments:**
> **username_0**: 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  
> **username_4**: Technically you can get any even degree, depending on whether you distinguish identical nodes formed from different clauses.  
> **username_0**: that should read "3 or more". ["degree"](http://en.wikipedia.org/wiki/Degree_(graph_theory)) is defined for undirected graphs, but what is "degree" defined as on a DAG? guess you mean ["indegree"](http://en.wikipedia.org/wiki/Indegree#Indegree_and_outdegree)? 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.  
> **username_4**: Indeed, I meant in-degree.  
> **username_0**: fyi, am accepting this answer because the question was **(unfairly) closed** & there is no opportunity for new, complete, creative etc. answers  

---

