1
$\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)$.

  1. Is there an algorithm to decide if a CNF is already in the reduced form or not?

  2. 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.

Improve this question
$\endgroup$
1
  • $\begingroup$ What did you do to find answers yourself? Do you see a connection to Logic optimisation? $\endgroup$
    – greybeard
    Commented Sep 14, 2020 at 5:38

1 Answer 1

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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