1
$\begingroup$

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.

Improve this question
$\endgroup$
15
  • 2
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Commented Feb 17, 2013 at 1:23
  • 6
    $\begingroup$ 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. $\endgroup$
    – Vijay D
    Commented Feb 17, 2013 at 1:38
  • 2
    $\begingroup$ @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. $\endgroup$
    – Kaveh
    Commented Feb 17, 2013 at 1:49
  • 4
    $\begingroup$ 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 ? $\endgroup$
    – Suresh Venkat
    Commented Feb 17, 2013 at 4:42
  • 6
    $\begingroup$ 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. $\endgroup$
    – Vijay D
    Commented Feb 18, 2013 at 5:25

1 Answer 1

Reset to default
5
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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 $\endgroup$
    – vzn
    Commented Feb 16, 2013 at 17:28
  • $\begingroup$ Technically you can get any even degree, depending on whether you distinguish identical nodes formed from different clauses. $\endgroup$
    – Shaull
    Commented Feb 16, 2013 at 17:33
  • $\begingroup$ 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. $\endgroup$
    – vzn
    Commented Feb 16, 2013 at 17:50
  • $\begingroup$ Indeed, I meant in-degree. $\endgroup$
    – Shaull
    Commented Feb 16, 2013 at 18:03
  • $\begingroup$ fyi, am accepting this answer because the question was (unfairly) closed & there is no opportunity for new, complete, creative etc. answers $\endgroup$
    – vzn
    Commented Feb 17, 2013 at 23:16

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