Hello forum! I have a computer science background, but my understanding of boolean expressions probably needs a refresher. I'm trying to write a program that takes a boolean expression and finds the minimal CNF or DNF for it.

Is there a general solution to this problem? I tried writing something that applied the boolean simplification rules, but it didn't work for all cases. Here is that attempt: https://github.com/tuzz/boolean_simplifier

How would such an algorithm work over something like this:

(a v b) ^ (-a v -(a ^ -a)) ^ a

 

I don't know the explicit algorithm (though I would guess you can find one on StackExchange), but I do want to warn you that the DNF version of an arbitrary boolean formula is highly likely to have EXP(n) clauses, where n is the number of variables in the original formula. This is why 3-SAT with CNF formulas is NP-complete but in P with DNF formulas, since encoding the formula in DNF in the first place is where the exponential growth happens.

 

I think you have two choices, either do minimalization using boolean rules, or you can try to implement Karnaugh maps, which might be eaiser to do correctly in code.

 

I think you have two choices, either do minimalization using boolean rules, or you can try to implement Karnaugh maps, which might be eaiser to do correctly in code.

K-maps will simplify a Boolean expression (give you the minimal form), but they won't put it into CNF/DNF.

 

Take a look at my blog on SOP and POS forms. That should give you a good path to constructing an approach to your problem.

For the example you cite, namely (a v b) ^ (-a v -(a ^ -a)) ^ a, most people here (myself most definitely included) are not used to working with this symbology, so let's switch it to something we can better relate to through the following mappings (and confirm that I am using the mappings that you intended):

- : inversion => NOT, thus -a => a'
^ : conjunction => AND, thus a ^ b => ab or (a)(b)
v : disjunction => OR, thus a v b => a+b

I'm also assuming that you have inversion having the highest precedence (other than parenthetical grouping) and that conjunction has precedence over disjunction. Beyond that I am assuming left to right associativity.

This converts your example to

(a + b) (-a + -[(a)(-a)]) (a)

The most straightforward approach, but it might explode computationally, would be to expand all of the products so that you have a purely sum of products form. This would result in:

[(a + b) (-a) + (a + b){-[(a)(-a)]}] (a)
(a + b) (-a)(a) + (a + b){-[(a)(-a)]}(a)
(a)(-a)(a) + (b)(-a)(a) + [ (a){-[(a)(-a)]} + (b){-[(a)(-a)]} ](a)
(a)(-a)(a) + (b)(-a)(a) + (a){-[(a)(-a)]}(a) + (b){-[(a)(-a)]}(a)

At this point you can apply DeMorgan's Theorem -(ab) = (-a)+(-b) to get:

(a)(-a)(a) + (b)(-a)( a) + (a)[-(a) + -(-a)]( a) + (b)[-(a) + -(-a)](a)

And now you can continue expanding:

(a)(-a)(a) + (b)(-a)( a) + [(a)(-(a)) + (a)(-(-a))]( a) + [(b)(-(a)) + (b)(-(-a))](a)
(a)(-a)(a) + (b)(-a)( a) + (-(a))( a) + (a)(-(-a))( a) + (b)(-(a))( a) + (b)(-(-a))(a)

Now you can apply the inversion properties, -(a) = -a and -(-a) = a, to get:

(a)(-a)(a) + (b)(-a)(a) + (-a)(a) + (a)(a)(a) + (b)(-a)(a) + (b)(a)(a)

Now you can reorder terms in lexical order with inverted forms immediately following non-inverted forms:

(a)(a)(-a) + (a)(-a)(b) + (a)(-a) + (a)(a)(a) + (a)(-a)(b) + (a)(a)(b)

Now you can apply the property that (a)(a) = (a) to remove duplicate factors:

(a)(-a) + (a)(-a)(b) + (a)(-a) + (a) + (a)(-a)(b) + (a)(b)

Now you can apply the properties (a)(-a) = 0 and (0)(a) = 0 to identify null terms:

0 + (0)(b) + 0 + (a) + (0)(b) + (a)(b)
0 + 0 + 0 + (a) + 0 + (a)(b)

Now to can apply the property that (0)(a) = 0 to remove the null terms:

(a) + (a)(b)

Now you can expand each term to add missing factors (i.e., be in normal form) by noting that (a)(1) = (a) and (a+a')=1, thus (a) = (a)(b+b'):

(a)(b+b') + (a)(b)

Now you can go through this process again:

(a)(b) + (a)(b') + (a)(b)
(a)(b) + (a)(b) + (a)(b')
(a)(b) + (a)(b')

Or, in your symbology:

(a ^ b) v (a ^ -b)

Note that this reduces to just (a), which agrees with your original expression with a bit of thought.

With a bit of inspection, you can choose a much, much better order in which to apply these theorems and reduce the steps to something more like:

(a + b) (-a + -[(a)(-a)]) (a)
(a + b) (-a + -(0)) (a)
(a + b) (-a + 1) (a)
(a + b) (1) (a)
(a + b)(a)
aa + ab
a + ab
a(b+b') + ab
ab + ab' + ab
ab + ab'