added 2SAT implementation - prunes redundant clauses (works out pretty fast - comparable to SCC)