Is there an algorithm for reducing CNFs further

Question

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.

Answer 1

CNF minimization is hard; see https://cstheory.stackexchange.com/q/9839/5038. It is certainly NP-hard, and there is a sense in which it is "even harder".

One way to get some intuition why it is hard is that if the CNF is not satisfiable, then its reduced form is "False", whereas if it is satisfiable, its reduced form is something else. So, if you had an efficient way to find a reduced form, that would immediately give you a way to tell whether the CNF is satisfiable -- a task that we know is NP-hard.

See https://cstheory.stackexchange.com/q/9839/5038 and https://en.wikipedia.org/wiki/Logic_optimization#Circuit_minimization_in_Boolean_algebra for some points into the literature on algorithms for this task.