Simplify boolean expression algorithm

Anybody knows of an algorithm to simplify boolean expressions?

I remember the boolean algebra and Karnaught maps, but 开发者_StackOverflow中文版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?

---

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.

---

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.

---

There are two parts to this problem, logical simplification and representation simplification.

For logical simplification, Quine-McCluskey. For simplification of the representation, recursively extract terms using the distribution identity (0&1|0&2) == 0&(1|2).

I detailed the process here. That gives the explanation using only & and |, but it can be modified to include all boolean operators.

---

Is the number of possible distinct values finite and known? If so you could convert each expression into a boolean expression. For instance if a has 3 distinct values then you could have variables a1, a2, and a3 where a1 being true means that a == 1, etc. Once you did that you could rely on the Quine-McCluskey algorithm (which is probably better for larger examples than Karnaugh maps). Here is some Java code for Quine-McCluskey.

I can't speak to whether this design would actually simplify things or make them more complicated, but you might want to consider it at least.

---

First shot using Google found this paper:

http://hopper.unco.edu/KARNAUGH/Algorithm.html

Of course, that does not deal with non-boolean subexpressions. But this latter part in its general form is really hard, since there is definitely no algorithm to check if an arbitrary arithmetic expression is true, false or whatever. What you are asking for goes deeply into the field of compiler optimization.

---

This is hard man. The algorithm in the simplest way that I found was match every output combination with each input each combination. But that's the basic algorithm, didn't solve every expression.

If all output (q1,q2,q3,q4) is same with for i.e input A combination then the result of simplification will be A.

If not, you will try another variabel / input dependency.