c++ linear formula simplifying library

Question

What is the best (in terms of simplicity of use and performance) C++/C++11 library which can simplify formulas like the following?

(a < 0 && b > 0) || (a < 0 && c > 0) || (a < 0 && c > 1) 

to (e.g.)

a < 0 && (b > 0 || c > 0)

I think it is very important to explain one thing (because I see this question is misunderstood).

I do not want to simplify C / C++ expressions - I know, the compiler can make it.

I'm making a graph processing tool. On the edges of the graph, there are some conditions about its vertices (lets say the vertices are a, b, c and these conditions are like a<b, b>0 etc - Please note, that these conditions are not expressed as "strings", they can be any function or library call). During processing, I'm collecting the expressions together and before further graph processing I want to simplify them.

The conditions and expressions will be created during runtime.

I want to be able to input some expressions to that library, like:

[...]
a = new Variable();
b = new Variable();
expr1 = lib.addExpr(a,0, lib.LESS);
expr2 = lib.addExpr(b,0, lib.MORE);
expr3 = lib.addExpr(expr1, expr2, lib.AND);
[...]
cout << lib.solve(exprn).getConditionsOf(a);

Of course this library will probably have a lot more beautiful API. I have written it as method calls only to show what I expect to be the underlying mechanism - to emphasize, that I do not need a source to source compiler or that this question is not related to source compilation optimization.

Moriarty

What is the "some conditions" that you are talking about(in response to gnzlbg), give us an example. – Nissie

Also, you do realize that x=simplifier.newVar() is a function call which is a lot more complicated than (x<y)||(y<1) right? I think you need to explain to us how are you planning on gaining from this exercise, your larger goal. – Nissie

Of course it is more complicated and this library (which i'm looking for) could have beautifull PAI alloowing me to write (x<y)||(y<1). This is notthe point of this question. We are looking for a solution, which will simplify expressions because we NEED the simplified form as an input to our algorithm – Tetratomic

I've updated the question, but I'm not his author (I'm working together with him, so it will appear after it will be reviewed). – Tetratomic

remdezx, I added to your question an edit originally written by @danilo2 (read the previous comment), because he claims he works with you on this. If this is not true, or if you do not like this edit, feel free to edit the question again. – Emanative

thanks for edit! It's exactly what we need :) – Moriarty

Answer 1

You are looking for a symbolic math library for C++ that can handle boolean logic.

Here are some to get started with:

• SymbolicC++: powerful, general purpose symbolic math library for C++, but not particularly intended for boolean mathematics.
• BoolStuff: not a general-purpose symbolic math library, very focused on boolean logic, but does probably exactly what you want.
• Logic Friday: standalone digital circuit analysis tool and boolean logic simplifier, with C API.

Seizure

Answer 2

If you first generate the truth table (fairly trivial), this reduces to the circuit minimization problem, which is well-studied.

Madonia

Reducing the truth table to a two-level logic circuit is well-studied. E.g. via Carnaugh maps and other algorithms. The OP is allowing arbitrary circuits. This is much harder and less studied. – Corset

Answer 3

Suggested Procedure

In lieu of a dedicated library, my suggested procedure for solving your problem is as follows:

1. Generate a truth table for the unsimplified Boolean expression.
2. Identify the cases where the single-variable comparison expressions imply other comparison expressions of the same variable. This should be straightforward if your use-case is fully representative.
3. Label the truth table outputs as "Do Not Care"s (DNCs) for those entries where the input values violate the implications.
4. Use the truth table as an input to a Boolean expression simplifier that supports truth tables and DNCs. As Mahmoud Al-Qudsi suggests, Logic Friday is a good candidate, and this is what I used in the example below.

Explanation

Assuming that your given use-case is fully representative of the problem space, then you can use any Boolean expression simplifier that supports truth table inputs and "Do Not Care" (DNC) function output specifications. The reason why DNCs are important is that some of your single-variable comparison expressions can imply other comparison expressions of the same variable. Consider the following single-variable comparison expression to Boolean variable mapping:

A = (a < 0); B = (b > 0); C = (c > 0); D = (c > 1);

D implies C or equivalently (not D or C) is always true. Therefore, when considering inputs to your example expression (substituting for our newly defined Boolean variable)

Output = (A && B) || (A && C) || (A && D)

we do NOT care about the inputs to this expression nor the output of this expression when (not D or C) is false because it can never happen. We can take advantage of this fact by generating the truth table for the above expression, and label the desired outputs as a DNC in the cases where (not D or C) is false. From that truth table, you use can the Boolean expression simplifier to generate the simplified expression.

Example

Let's apply the procedure to your example assuming the single-variable comparison expression to Boolean variable mapping given above. In particular, we have

Output = (A && B) || (A && C) || (A && D)

which maps to truth table I below. However, from your example, we know (not D or C) is always true; therefore, we can label all outputs where (D and not C) as DNC which leads to truth table II below.

Truth Table I               Truth Table II
=============               ==============
A  B  C  D  Output          A  B  C  D  Output
0  0  0  0    0             0  0  0  0    0
0  0  0  1    0             0  0  0  1   DNC
0  0  1  0    0             0  0  1  0    0
0  0  1  1    0             0  0  1  1    0
0  1  0  0    0             0  1  0  0    0
0  1  0  1    0             0  1  0  1   DNC
0  1  1  0    0             0  1  1  0    0
0  1  1  1    0             0  1  1  1    0
1  0  0  0    0             1  0  0  0    0
1  0  0  1    1             1  0  0  1   DNC
1  0  1  0    1             1  0  1  0    1
1  0  1  1    1             1  0  1  1    1
1  1  0  0    1             1  1  0  0    1
1  1  0  1    1             1  1  0  1   DNC
1  1  1  0    1             1  1  1  0    1
1  1  1  1    1             1  1  1  1    1

Plugging in truth table II into Logic Friday and using its solver yields the minimized (CNF) expression:

A && (B || C)

or equivalently, mapping back from Boolean variables,

a < 0 && (b > 0 || c > 0).

Rifleman

+1 for a lot of work... But +- the same is in the link in @dspeyer's post – Restrict

I disagree. While @dspeyer's post states that the problem can be reduced to a circuit minimization problem, the post does not provide details on how this reduction can be performed. Without elaborating further, the implication is that one should stop at truth table I and use that as the input to the solver. – Rifleman

Answer 4

I suggest you to build a decision tree.

Each of your condition divides number space into two sections. For example c > 1 divides space into (-Infinity, 1] and [1, +Infinity) sections. If you have another condition with c for example c>0 then you have extra division point 0 and finally you get 3 sections: (-Infinity, 0], [0,1] and [1, +Infinity).

So, each tree level will contain appropriate branching:

c<0
   b<0
      a<0
      a>0  
   b>0
      a<0
      a>0  
0<c<1
   b<0
      a<0
      a>0  
   b>0
      a<0
      a>0  
c>1
   b<0
      a<0
      a>0  
   b>0
      a<0
      a>0  

Now you should leave only that paths, which exist in your expression. This will be your optimization. Not sure it is 100% efficient, but it is somehow efficient.

In your case it will be

c<0
   b<0: false
   b>0
      a<0: true
      a>0: false  
0<c<1
   b<0
      a<0: true
      a>0: false  
   b>0
      a<0: true
      a>0: false  
c>1
   b<0
      a<0: true
      a>0: false  
   b>0
      a<0: true
      a>0: false  

To improve optimization you can introduce subtree comparison and union equivalent subtrees into one

c<0
   b<0: false
   b>0
      a<0: true
      a>0: false  
c>0
   a<0: true
   a>0: false  

Finally, when you receive your values, just trace the tree and check your decision. If you get a dead end (deleted path) then result is false. Otherwise you trace to exit and result will be true.

Drusie

Answer 5

You might be able to get what you want from a BDD library. BDDs don't quite give you a C++ expression at the end, but they give you a graph from which you can contsruct a C++ expression.

I've never used it, but I've heard minibdd is easy to use. See http://www.cprover.org/miniBDD/

Slavery

from the main site "It's not very efficient (the nodes use too much memory), and it is missing a lot of features" I dont think it is good solution for this question (especially when performance is one of the needed things) – Tetratomic

Pretty sure any BDD library you can find will simplify any boolean expression you could care to write by hand. (One thing it won't handle is noticing that c>0 || c>1 simplifies to c>0, though, so I guess this isn't such a good answer.) – Slavery

Answer 6

The best tool for simplifying that expression is your compiler's optimizer.

As far as I know no c++ library will rewritte such an expression for you (although it would be technically possible to write one using expression templates).

I would suggest to look at the assembly code produced by your compiler with high optimizations. It might give you a hint. Another alternative is provided by static analysis tools.

Hyaluronidase

You completly misundersteand the problem. We have several conditions as an input to our program. We want to simplicity them and then process them. So these conditions are NOT compile time constant and the simpliefied version is needed for further processing. – Tetratomic

We do not want any library to "rewrite it". We want to be able to set some conditions (with a special library methods) and then I want to get simplified version, which i could investigate with our c++ program. something like x=simplifier.newVar(); y=simplifier.newVar(); expr=simplifier.newExpr(); expr.addConstraint(a,b,simplifier.LESS); ... ... simplifier.siplify().getConstrainsOf(x); – Tetratomic

@danilo2 Sorry I misunderstood your question and thanks for updating it with a better description, it is really interesting! – Hyaluronidase