A propositional formula in conjunctive normal form (from now on abbreviated CNF) is said to be in standard form if there are no pure literals, no duplicated clauses, and no possible resolutions in which the resolvent is shorter (by literal count) than one of the operands.
The problem is to show that a 2CNF in standard form with n variables and n clauses is satisfiable.
I am not really sure how I am supposed to make use of the hypothesis that there are as many variables as clauses. The only conclusion that I have been able to draw is that for every variable there must be at least one clause that does not contain the variable--the proof is by contradiction and uses the pigeonhole principle. I also tried using Hall's theorem to show that there is a matching from clauses to variables--which would then give us a satisfying assignment--but I have come to believe that this may in fact not be true in general.