Simplify boolean expression algorithm

Question

Anybody knows of an algorithm to simplify boolean expressions?

I remember the boolean algebra and Karnaught maps, but this is meant for digital hardware where EVERITHING is boolean. I would like something that takes into account that some sub-expressions are not boolean.

For example:

a == 1 && a == 3

this could be translated to a pure boolean expression:

a1 && a3 

but this is expression is irreducible, while with a little bit of knowledge of arithmetics everibody can determine that the expression is just:

false

Some body knows some links?

Answer 1

You might be interested in K-maps and the Quine–McCluskey algorithm.

I think SymPy is able to solve and simplify boolean expressions, looking at the source might be useful.

Answer 2

Your particular example would be solved by an SMT solver. (It'd determine that no setting of the variables could make the expression true; therefore it's always false. More-general simplification is out of scope for such solvers.) Showing that an expression is equivalent to true or false is of course NP-hard even without bringing arithmetic into the deal, so it's pretty cool that there's practical software for even this much. Depending on how much arithmetic knowledge is in scope, the problem may be undecidable.