Regarding the question of suitability for this site:
I do not believe the question in its present form is well worded. I am ambivalent about its appropriateness. Ill formed questions appear occasionally on this site. I myself have posted a question that was sub-optimal for the site, and was glad that the community engaged me and pointed out why my question was inappropriate rather than closing it. I believe the community has tolerated and helped to improve vague, unclear, but well intentioned questions. Even if intent is unclear, we have helped improve unclear questions. I feel that this question can easily be improved to a clear, technical question and ideally, I would prefer this route.
I am aware that the OP is very unlikely to incorporate feedback from the community and improve the question. I agree that this is a problem and sympathise with the frustration of both the site users, and particularly moderators who must confront such issues.
Nevertheless, I would prefer to be part of a relaxed community. This is a personal preference. I am averse to forums that feature flame wars, heavy moderation and contentious discussions that essentially amount to shouting contests for intellectual bullies. I would like this site to have an image that is welcoming and not intimidating to give computer scientists the confidence that they can ask questions and be listened to rather than fear admonishment if their query does not satisfy some rigid set of rules. Let me clarify that I am currently fairly happy with this site and I do not believe any of the concerns I am stating currently apply.
Closing a question so quickly, especially when it is not obvious why (to me as a user, viewing the question) feels strong to me. I would have preferred for the community to go through the potentially futile process of suggesting improvements and then either expressing our displeasure with our votes, or ignoring the question beyond a point. To Kaveh, I would like to further add that this is a preference of mine, not a strong opinion. My desire for a relaxed environment and concern that closing a few questions quickly will cause us to descend into a dictatorship is less realistic than your concern that the site will attract cranks, but neither concern seems empirically justified. In the latter case, you may have more information as a moderator and if people are indeed being driven away by cranks I would agree that we should behave proactively. This concern does not seem to apply to this question because the user in question has been on the site for a while and the community has survived.
Regarding improving the question itself.
Here is one potential wording.
This question is about the combinatorial structure of resolution proofs.
Let $Prop$ be a set of atomic propositions. A literal is an atomic proposition or its negation. A clause is a disjunction of literals. Let $Clause$ be the set of clauses over $Prop$.
The resolvent of two clauses $C \lor p$ and $\neg p \lor D$ with pivot $p$ is the clause $C \lor D$.
A resolution proof is a finite, labelled DAG $P = (V, E, piv, clause)$, where
- $(V,E)$ is a graph in which vertices have in-degree $0$ or $2$, and vertices with in-degree $0$ are called leaves and those with in-degree $2$ are called internal vertices
- $piv$ is a function from internal vertices to atomic propositions
- $clause: V \to Clause$ is a function satisfying that for all internal vertices $w$ with incoming edges from $u$ and $v$, $clause(w)$ is the resolvent of $clause(u)$ and $clause(v)$ with pivot $pivot(w)$.
A clause $C$ is derived by resolution from a set of clauses $F$ if there exists a resolution proof $P$ in which $clause(v)$ is $C$ for some vertex $v$ and every leaf vertex on a path to $v$ is labelled with a clause from $F$. A resolution refutation is a derivation of the empty clause.
The original questions can be reformulated as below.
- For every DAG $G$, does there exist a resolution proof $P$ whose underlying graph is isomorphic to $G$?
- For every DAG $G$, does there exist a resolution refutation $P$ whose underlying graph is isomorphic to $G$?
- Does there exist an ordering on clauses such that the set of clauses labelling leaves is minimal with respect to that ordering?
Let me point out that I believe (1) and (2) are directly in the question and (3) includes a minor interpretation on my part. I would further extend (3) as below.
3'. If $E$ and $F$ are sets of clauses, define the order $E \le F$ if for every clause $C$ in $E$ there exists a clause $D$ in $F$ such that every literal in $C$ occurs in $D$. For every DAG $G$, does there exist a proof $P$ such that the clauses labelling leaves are minimal with respect to this order. Is there a unique minimum labelling?
My reformulation does leave open whether the question is research level. I believe the reformulated question is not difficult to answer, but I find it appropriate for this site. The proof required would be a background exercise for approaching the type of work in The complexity of resolution refinements.