Boolean expression solver/simplifier

Question

I am looking for an Boolean expression solver for very big (but not complex) algebra like: Boolsche Ausdrücke vereinfachen (Axiome) I would like to have some code (c++ or java [or libraries]) to simplify huge boolean expression. I haven´t found something. I just want to do some "simply" convertion like:

a && ~a -> 0

a || a && (b || c) -> a

But much longer. And I want to use symbolics (a, b, c1, d1..) not TRUE, FALSE, 0 or 1 at the moment. Thank you in advance.

Edit: If I write it my self, I could use Javaluator and evaluate. When I have: (adb+c) && d I would like to start with multiply out. Anyone an idea?

Answer 1

My favorite tool for such tasks is Logic Friday 1. It is free for non-commercial use.

Logic Friday 1 accepts Boolean expressions as formula and as truth table. It includes compiled binaries of Berkeley tools Espresso and misII. The latter is being used for multi-level functions.

Another tool is bc2cnf. It reads a boolean expression (or a set of expressions) as a "circuit" and translates it to conjunctive normal form (CNF), basically a product of OR-expressions. bc2cnf applies some simplification rules during this translation. For expressions of modest size it would be an option to convert the CNF to disjunctive normal form (DNF) and use Espresso to get a minimized form.