Reducing a boolean expression

Question

I am having an expression, suppose,

a = 1 && (b = 1 || b != 0 ) && (c >= 35 || d != 5) && (c >= 38 || d = 6)

I expect it to be reduced to,

a = 1 && b != 0 && (c >= 38 || d = 6)

Does anyone have any suggestions? Pointers to any algorithm?

Nota Bene: Karnaugh Map or Quine-McCluskey are not an option here, I believe. As these methods don't handle grey cases. I mean, expression can only be reduced as far as things are like, A or A' or nothing, or say black or white or absense-of-colour. But here I'm having grey shades, as you folks can see.

Solution: I have written the program for this in Clojure. I used map of a map containing a function as value. That came pretty handy, just a few rules for a few combinations and you are good. Thanks for your helpful answers.

Answer 1

I think you should be able to achieve what you want by using Constraint Handling Rules. You would need to write rules that simplify the OR- and AND-expressions.

The main difficulty would be the constraint entailment check that tells you which parts you can drop. E.g., (c >= 35 || d != 5) && (c >= 38 || d = 6) simplifies to (c >= 38 || d = 6) because the former is entailed by the latter, i.e., the latter is more specific. For the OR-expressions, you would need to choose the more general part, though.

Google found a paper on an extension of CHR with entailment check for user-defined constraints. I don't know enough CHR to be able to tell you whether you would need such an extension.

Answer 2

I believe these kinds of things are done regularly in constraint logic programming. Unfortunatly I'm not experienced enough in it to give more accurate details, but that should be a good starting point.

The general principle is simple: an unbound variable can have any value; as you test it against inequalities, it's set of possible values are restricted by one or more intervals. When/if those intervals converge to a single point, that variable is bound to that value. If, OTOH, any of those inequalities are deemed unsolvable for every value in the intervals, a [programming] logic failure occurs.

See also this, for an example of how this is done in practice using swi-prolog. Hopefully you will find links or references to the underlying algorithms, so you can reproduce them in your platform of choice (maybe even finding ready-made libraries).

Update: I tried to reproduce your example using swi-prolog and clpfd, but didn't get the results I expected, only close ones. Here's my code:

?- [library(clpfd)].
simplify(A,B,C,D) :-
    A #= 1 ,
    (B #= 1 ; B #\= 0 ) ,
    (C #>= 35 ; D #\= 5) ,
    (C #>= 38 ; D #= 6).

And my results, on backtracking (line breaks inserted for readability):

10 ?- simplify(A,B,C,D).

A = 1,
B = 1,
C in 38..sup ;

A = 1,
B = 1,
D = 6,
C in 35..sup ;

A = 1,
B = 1,
C in 38..sup,
D in inf..4\/6..sup ;

A = 1,
B = 1,
D = 6 ;

A = 1,
B in inf.. -1\/1..sup,
C in 38..sup ;

A = 1,
D = 6,
B in inf.. -1\/1..sup,
C in 35..sup ;

A = 1,
B in inf.. -1\/1..sup,
C in 38..sup,
D in inf..4\/6..sup ;

A = 1,
D = 6,
B in inf.. -1\/1..sup.

11 ?- 

So, the program yielded 8 results, among those the 2 you were interested on (5th and 8th):

A = 1,
B in inf.. -1\/1..sup,
C in 38..sup ;

A = 1,
D = 6,
B in inf.. -1\/1..sup.

The other were redundant, and maybe could be eliminated using simple, automatable logic rules:

1st or 5th ==> 5th          [B == 1  or B != 0 --> B != 0]
2nd or 4th ==> 4th          [C >= 35 or True   --> True  ]
3rd or 1st ==> 1st ==> 5th  [D != 5  or True   --> True  ]
4th or 8th ==> 8th          [B == 1  or B != 0 --> B != 0]
6th or 8th ==> 8th          [C >= 35 or True   --> True  ]
7th or 3rd ==> 3rd ==> 5th  [B == 1  or B != 0 --> B != 0]

I know it's a long way behind being a general solution, but as I said, hopefully it's a start...

P.S. I used "regular" AND and OR (, and ;) because clpfd's ones (#/\ and #\/) gave a very weird result that I couldn't understand myself... maybe someone more experienced can cast some light on it...