I have a boolean formula in conjunctive normal form (CNF): $(a\vee b \vee c) \wedge (a \vee b \vee \neg c) \wedge (x \vee y)$
I know that this can be simplified to: $(a\vee b)\wedge (x \vee y)$.
a) Is there an algorithm to decide if a CNF is already in the reduced form or not?
b) Is there an algorithm that can do this reduction in an manner more efficient than comparing each pair of clauses to see if any pairing can be reduced? I wish to automate this reducing for any CNF and am looking for any algorithms that I can borrow/implement.