C++ lineare Formel, die Bibliothek vereinfacht

Question

Was ist das Beste (in Bezug auf Einfachheit der Verwendung und Leistung) C++/C++ 11-Bibliothek, die Formeln wie folgt vereinfachen können?

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

zu (z)

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

Ich denke, es ist sehr wichtig, eine Sache zu erklären (denn ich sehe diese Frage falsch verstanden ist).

Ich möchte C/C++ - Ausdrücke nicht vereinfachen - ich weiß, der Compiler kann es machen.

Ich mache ein Grafik-Bearbeitungs-Tool. An den Kanten des Graphen gibt es einige Bedingungen für seine Eckpunkte (sagen wir die Eckpunkte sind a, b, c und diese Bedingungen sind wie a<b, b>0 etc - Bitte beachten Sie, dass diese Bedingungen nicht als "Strings" ausgedrückt werden, sie kann jede Funktion oder Bibliotheksaufruf sein). Während der Verarbeitung sammle ich die Ausdrücke zusammen und vor der weiteren Graph-Verarbeitung möchte ich sie vereinfachen.

Die Bedingungen und Ausdrücke werden zur Laufzeit erstellt.

Ich möchte diese Bibliothek einige Ausdrücke Eingang zu können, wie:

[...] 
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); 

Natürlich ist diese Bibliothek wird wahrscheinlich viel schönere API haben. Ich habe es als Methodenaufrufe geschrieben, nur um zu zeigen, was ich als zugrunde liegenden Mechanismus erwarte - zu betonen, dass ich keinen Quelle-zu-Quelle-Compiler benötige oder dass diese Frage nicht mit der Quellkompilierungsoptimierung zusammenhängt.

Answer 1

Sie können möglicherweise von einer BDD-Bibliothek bekommen, was Sie wollen. BDDs geben am Ende nicht wirklich einen C++ - Ausdruck, aber sie geben Ihnen ein Diagramm, aus dem Sie einen C++ - Ausdruck hervorheben können.

Ich habe es nie benutzt, aber ich habe gehört, Minibdd ist einfach zu bedienen. Siehe http://www.cprover.org/miniBDD/

Answer 2

Das beste Werkzeug zur Vereinfachung dieses Ausdrucks ist der Optimierer Ihres Compilers.

Soweit ich weiß, wird keine C++ - Bibliothek einen solchen Ausdruck für Sie neu schreiben (obwohl es technisch möglich wäre, einen mit Expression-Templates zu schreiben).

Ich würde vorschlagen, den Assemblercode, der von Ihrem Compiler mit hohen Optimierungen erstellt wurde, zu betrachten. Es könnte dir einen Hinweis geben. Eine weitere Alternative bieten statische Analysewerkzeuge.

Answer 3

Wenn Sie zuerst die Wahrheitstabelle erstellen (ziemlich trivial), reduziert dies auf die circuit minimization problem,, die gut untersucht ist.

Answer 4

Sie suchen nach einer symbolischen Math-Bibliothek für C++, die boolesche Logik verarbeiten kann.

Hier sind einige, mit zu beginnen:

• SymbolicC++: leistungsfähige Allzweck symbolischen Mathematik-Bibliothek für C++, aber nicht besonders für boolean Mathematik gedacht.
• BoolStuff: keine allgemeine symbolische Math-Bibliothek, sehr auf Boolesche Logik konzentriert, aber wahrscheinlich genau das, was Sie wollen.
• Logic Friday: Standalone Digital Circuit Analyse-Tool und Boolean Logic Simplifier, mit C-API.

Answer 5

vorgeschlagene Verfahren

Anstelle einer eigenen Bibliothek, mein vorgeschlagenen Verfahren Ihr Problem zu lösen, ist wie folgt:

1. eine Wahrheitstabelle für die nicht vereinfachten Booleschen Ausdruck generieren.
2. Identifizieren Sie die Fälle, in denen die Vergleichsausdrücke mit einer Variablen andere Vergleichsausdrücke derselben Variablen implizieren. Dies sollte einfach sein, wenn Ihr Anwendungsfall vollständig repräsentativ ist.
3. Beschriften Sie die Ausgaben der Wahrheitstabelle als "Nicht relevant" (DNCs) für die Einträge, bei denen die Eingabewerte die Implikationen verletzen.
4. Verwenden Sie die Wahrheitstabelle als Eingabe für einen vereinfachenden Booleschen Ausdruck, der Wahrheitstabellen und DNCs unterstützt. Wie Mahmoud Al-Qudsi vorschlägt, ist Logic Friday ein guter Kandidat, und das habe ich im folgenden Beispiel verwendet.

Erklärung

Unter der Annahme, dass Ihre gegebenen Anwendungsfall des Problems Raum vollständig repräsentativ ist, dann können Sie einen beliebigen Booleschen Ausdruck simplifier verwenden, die Eingänge Wahrheitstabelle unterstützt und „Do not Care“ (DNC) Funktionsausgang Spezifikationen. Der Grund, warum DNCs wichtig sind, besteht darin, dass einige Ihrer Vergleichsausdrücke für eine Variable andere Vergleichsausdrücke derselben Variablen implizieren können. Betrachten Sie den folgenden Single-Variable Vergleichsausdruck Variable Mapping Boolean:

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

D impliziert C oder äquivalent (nicht D oder C) ist immer wahr. Wenn daher Eingänge zum Beispiel Ausdruck (Substitution für unsere neu definierte Boolesche Variable)

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

bedenkt, dass wir zu diesem Ausdruck nicht über die Eingänge sorgen noch den Ausgang dieses Ausdrucks, wenn (nicht D oder C) falsch ist weil es nie passieren kann. Wir können diese Tatsache nutzen, indem wir die Wahrheitstabelle für den obigen Ausdruck erzeugen und die gewünschten Ausgaben als DNC in den Fällen bezeichnen, in denen (nicht D oder C) falsch ist. Aus dieser Wahrheitstabelle können Sie den booleschen Ausdruck simplifier verwenden, um den vereinfachten Ausdruck zu generieren.

Beispiel

Lassen Sie sich das Verfahren zu Ihrem Beispiel gilt den einzelnen variablen Vergleichsausdruck unter der Annahme, variable Zuordnung oben angegebenen Boolean. Insbesondere haben wir

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

, die Wahrheitstabelle I unten zugeordnet. Wie auch immer, von Ihrem Beispiel wissen wir (nicht D oder C) ist immer wahr; Daher können wir alle Ausgänge mit (D und nicht C) als DNC bezeichnen, was zur Wahrheitstabelle II führt.

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 

Anstecken Wahrheitstabelle II in Logic Freitag und mit seiner Solver ergibt das minimiert (CNF) Ausdruck:

A && (B || C) 

oder äquivalent Mapping zurück von Booleschen Variablen,

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

Answer 6

Ich schlage vor, dass Sie einen Entscheidungsbaum bauen.

Jede Ihrer Bedingungen unterteilt den Nummernraum in zwei Abschnitte. Zum Beispiel c > 1 teilt Raum in (-Infinity, 1] und [1, +Infinity) Abschnitte. Wenn Sie eine andere Bedingung mit c zum Beispiel c>0 haben, dann haben Sie zusätzlichen Teilungspunkt 0 und schließlich erhalten Sie 3 Abschnitte: (-Infinity, 0], [0,1] und [1, +Infinity).

So wird jeder Baumebene entsprechende Verzweigung enthalten:

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 

Jetzt sollten Sie lassen nur die Pfade, die in ihrem Ausdruck existieren. Dies wird Ihre Optimierung sein. Nicht sicher, es ist 100% effizient, aber es ist irgendwie effizient.

In Ihrem Fall wird es

sein

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 

Optimierung verbessern Sie subtree Vergleich und Vereinigung äquivalente Teilbäume in einem

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

schließlich den Baum vorstellen können, wenn Sie Ihre Werte erhalten, nur Spuren und überprüfe deine Entscheidung. Wenn Sie eine Sackgasse (gelöschten Pfad) erhalten, ist das Ergebnis false. Andernfalls verfolgen Sie, um zu beenden und das Ergebnis wird true sein.