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.

Smolt

There are limits to how much reduction can be done in polynomial time. For example, if you could always reduce any conjunctive normal form expression to its simplest form, you would have solved the open 3SAT problem. – Aaberg

@mbeckish: That sounds scary to me. Actually, I didn't know about these things until you folks steered me to the right direction. I was thinking of not just 3SAT, but nSAT problems. Now, it all sounds impossible. – Smolt

Do not be afraid to tackle NP-hard problems. For most of them, the hard part will be in a relatively small area of the problem space, in the phase transition between infeasible and easy problems. If solving NP-hard problems was always impossible, I would be out of my job. It much depends on how far you expect your algorithm to scale. – Throughway

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.

Throughway

After reading briefly on Constraint Programming, then Constraint Logic Programming (mgibsonbr pointed out in another post), then Constraint Satisfaction Problems, then Constraint Handling Rules, and then Constraint Optimisation, I believe that my problem lies under Constraint Optimisation, and I also believe that any backtracking algorithm would be useful. I am particularly looking into B&B, and Bucket Elimination, where the latter is not a backtracking algo. Am I going in the right direction? – Smolt

@AdeelAnsari: Yes, you can see it as a kind of optimisation problem if you take the number of clauses as the measure and you want to find the shortest representation. Usually, B&B is a good choice when solving COP problems, but will only help if you can compute some lower bound for the number of clauses in the final result, else it's complete search. Backtracking will be included when using CLP. CHR is intended to be "committed-choice", i.e. w/o backtracking, but CHR implementations on top of CLP actually do have backtracking (e.g. in ECLiPSe). Whether bucket elimination helps, I don't know. – Throughway

@AdeelAnsari: btw, are you looking for a completely generic solution, or are you working on a solution for a specific use case? If the latter, how many variables and what domain size will you have to deal with? – Throughway

Take it as a if-clause in a program function, or a where-clause in a sql-select statement. I am trying to reduce the constraints, if some entail some others, in that condition. I don't think, I can fix the size of variables. – Smolt

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

Emersion

Thanks, pal. It's very nice of you. I'm looking into it, and trying to digest. – Smolt