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.