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.
in SAT resolution proofs, are all DAGs possible?
cc.complexity theory;reference request;graph theory;proofs;np complete
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).