0
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

I posted the same question to the CS stack exchange and received an answer for this question: https://cs.stackexchange.com/a/130043/126327

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.